Skip to content

Get rid of tvProp by using thread identifiers and ghost state.

Jacques-Henri Jourdan requested to merge no_tvprop into master

Having to deal with two logics (tvProp and vProp) in LambdaRust-weak is tedious. This basically mean using embeddings all over the place, and sometimes it is also needed to use the "unembedding" (for using WP within vProp).

This MR is an attempt at getting rid of tvProp, so that everything can be done in vProp. The trick is that the only relevant frel and acq views are the current one of some thread. So, we associate to an authoritative ghost variable the current view of each thread, and refer to this ghost state in the definition of the acquire and release modalities.

This requires changing the definition of WP and of the acquire and release modalities, and make them depend on the thread identifier (I am open to suggestions if you think the notations can be improved), so that they both refer to the ghost variable containing the current view of the thread.

Cons:

The definition of WP requires up-closure again because of the authoritative view, and I do not know how to fix that. This means that the hard work we did a few month ago for getting rid of this up closure can no longer be used. Still, I think that this is a good thing that we made sure that the promising semantics is monotonic.

One has to refer to thread identifiers in WP, which make everything around WP a little bit more complicated.

One might wonder whether this new formalism is less expressive than the one using tvProp. Up to now, the only uses of the release and acquire views were the release and acquire modalities. And the only release and acquire views that were used were those of a thread. In this proposal, these modalities can still be defined and they follow the same reasoning rules. Moreover, we can still refer to the release and acquire views of a thread via the ghost state. The only issue that I can foresee is that one will no longer transfer an acquire/release modality between a thread and its child, since the thread ID will be different. But actually, I am not even convinced our formalization of the promizing semantics is sound to that respect. If I am not mistaken, this correspond to the following example:

x := 0    y := 0

y :={pln} 1        |
RelFence           |   a :={rlx} x
fork (             |   fork (
  x :={rlx} 1      |      AcqFence
)                  |      if  a == 1 then y :={pln} 2  
                   |   )
                   |

Is that UB? That is, is there a race between the two writes to y? If there were no fork, then the answer is that the rel/rlx/acq sequence ensure synchronization (right ?). But in the current example, the barriers and the relaxed accesses do no happen in the same thread, so that it is not clear that the synchronization happens.

Another (not really related) concern: In the logic, we never use the (location-relative) rel views. Does that mean that we miss something important?

Merge request reports