Ego-Lane-Derived-Digests for Privatizations: ProtectionBasedTIDPriv

[michael-schwarz]

Introduces one of the new privatizations which will need to be evaluated for my thesis. This might actually be a lightweight interesting instance that might be worth evaluating it in practice.

This takes the protection based analysis and replaces [g] and [g]' by [g,A] and [g,A]' respectively, where A is an ego-lane derived digest.

Implementation-wise we once more use the Reduced-Cardinal-Powerset construction and change types of unknowns from ValD to partial maps Digest -> ValD with default value bot.

TODO:

• Add new interesting tests
• Modify TID.is_must_parent. Currently, this is reflexive, which is against intuition (I rarely think of myself as my own father)

[michael-schwarz]

I was able to cast this as a generic lifter, which means we get no additional code duplication here 😄

[sim642]

Why does protection-tid use different digests than mutex-meet-tid?

[michael-schwarz]

The difference is that mutex-meet-tid is equipped with a L component that guarantees that all join-local contributions are already accounted for. protection-tid instead does not track such a component and thus needs to rely purely on the refinement provided by the ego-lane-derived digest. I'll add a comment to this effect.

[sim642]

But the digest modules don't have access to mutex-meet-tid's L, so how can it be coupled with that? Also in more-traces, the digest framework is introduced before L.

[michael-schwarz]

Yes, but things such as not reading from yourself and not reading from joined threads goes beyond what the digests can do, and relies on the analysis taking care of it in some way.

Consider e.g. reading from a thread that has been joined: It is possible that this thread held the mutex last before me, and thus the digests are compatible.
It is only because the analyses also read from some L that this contribution is accounted_for.

[michael-schwarz]

In more-traces this is the difference between
$$[[lock(a)]]^\sharp_\mathcal{A}(A_0,A_1) = \emptyset$$

and

$$\textsf{acc} A_0 A_1$$

[sim642]

Thanks for the explanation. I guess the coupling is kind of implicit here: this accounted_for assumes that the privatization actually accounts for things in its thread_join.