Define Missing TID Variants of Non-Relational Privatizations

[michael-schwarz]

As the TID digests are ego-lane derived and we now have a clear understanding of how privatizations that do not incorporate information at the same places as the concrete semantics can be refined by such digests, it would make sense to implement such refinement for:

• Protection-Based Reading
• Lock-Centered (if the proof goes through)
• Write-Centered
• Combined (if Lock-Centered succeeds)

Mutex-Oplus and Mutex-Meet admit general digests and are already refined in this manner.

The original analysis as proposed by Miné in 2012 did not have a notion of dynamically created thread IDs but did have reasoning about uniqueness. The setting is thus sufficiently dissimilar that it does not really seem to make sense to integrate our TIDs into that.

The handling of joins as for our ESOP paper requires a dedicated argument and construction (it is not a straightforward refinement and the refinement one can use to argue that it is sound seems to be not ego-lane derivered), so I would not integrate this here.