Parametrize Omega by the thread_id

This change is required for the dataraces since there Omega needs to refer to the current thread id. In particular, Omega should refer to a different thread_id after forking (which is not possible without this change).

theories/simplang/examples/data_races.v

@@ -27,7 +27,7 @@ Section data_race.
     )%E.
 
   Lemma remove_store_and_load_sim π:
-    ⊢ sim_ectx val_rel π remove_store_and_load_opt remove_store_and_load val_rel.
+    ⊢ sim_ectx (const val_rel) π remove_store_and_load_opt remove_store_and_load val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 
@@ -75,7 +75,7 @@ Section data_race.
     )%E.
 
   Lemma reg_promote_loop_sim π f:
-    ⊢ sim_ectx val_rel π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
+    ⊢ sim_ectx (const val_rel) π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 
@@ -119,7 +119,7 @@ Section data_race.
     )%E.
 
   Lemma hoist_load_sim π:
-    ⊢ sim_ectx val_rel π hoist_load_opt hoist_load val_rel.
+    ⊢ sim_ectx (const val_rel) π hoist_load_opt hoist_load val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 

[Ralf Jung]

Why not actually change val_rel to have the desired type? That'd avoid all users having to care about this...

I assume val_rel in the future needs to depend on the thread ID?

[Michael Sammler]

On my branch, val_rel still has type val → val → PROP. I use that to define weak_val_rel which additionally talks about the thread id (https://gitlab.mpi-sws.org/iris/simuliris/-/blob/msammler/dataraces/theories/simplang/heap_bij_races.v#L1053), but there are quite a few cases where one still needs val_rel instead of weak_val_rel. (E.g. the values in the heap bijection are related with val_rel, not weak_val_rel.)

[Ralf Jung]

What I mean is: I don't think we should have const val_rel everywhere. If that relation is widely used, it should have a name. And since the name is repeated a lot, it should be a short one -- val_rel seems good.

The thing only used in state_interp can have a longer name.

[Michael Sammler]

I agree that the repeated const val_rel is a bit annoying. I've fixed it in the other example by using a notation like we do else where. This file will actually change to use a weak_val_rel instead of const val_rel on my branch, so there is already a separate definition. Note that both weak_val_rel and val_rel are visible outside of the state interpretation and val_rel is probably used more often (weak_val_rel is only really relevant for the calls).

[Ralf Jung]

This file will actually change to use a weak_val_rel instead of const val_rel on my branch

That doesn't even typecheck. Do you mean const weak_val_rel? But I don't understand why that would ever be used.

[Michael Sammler]

No, I mean weak_val_rel. Both weak_val_rel and const val_rel have type thread_id → val → val → PROP. But weak_val_rel should probably be named differently, maybe ext_rel ? (because this is the relation for interacting with external functions)

[Ralf Jung]

weak_val_rel should probably be named differently, maybe ext_rel ? (because this is the relation for interacting with external functions)

Sounds like this is the value relation, and should thus be called val_rel.

The point of the value relation is to relate values that are passed to and returned from external functions, and the final return value for the top-level observation. So whatever relation does that job, should be called val_rel.

[Michael Sammler]

The point is that what I call ext_rel is not just relating the values that are passed from and to external functions. It also contains additional ghost state (weak_col π c in my case) that does not have anything to do with the values that are passed. The relation that relates the values would still be called val_rel.

[Ralf Jung]

I don't follow. It is still a relation that is satisified each time values are passed across an external boundary. The fact that it has a component that is independent of values is immaterial: this is still most definitely the thing that is called the "value relation" in the typical logical relation setup, or is it not?

[Ralf Jung]

The thing that does not contain weak_col (what's "col" for? the only association I have is "column" -- so maybe this should also get a more self-explaining name ;) should then get a different name. IIRC this is about executing synchronization instructions, so maybe it should be called val_rel_nosync (and weak_col should probably also have sync somewhere in its name)?

[Michael Sammler]

I am not sure which of the two relations corresponds to the value relation in typical logical relations. Maybe it makes more sense to continue this bikeshedding at some meeting. At that occasion we could also find a better name for weak_col (which I agree is not a good name).

[Ralf Jung]

I am not sure which of the two relations corresponds to the value relation in typical logical relations.

I think it's pretty clear: it's the thing that shows up in expr_rel and the key soundness theorems.

Maybe it makes more sense to continue this bikeshedding at some meeting. At that occasion we could also find a better name for weak_col (which I agree is not a good name).

Well, I think there's a concrete change you should do in this MR: don't use const val_rel, instead change the definition of val_rel to already be what everyone needs.

[Ralf Jung]

Specifically, I think expr_rel should look like this after this MR -- do you agree (up to alpha renaming)?

  Definition expr_rel e_t e_s : iProp Σ :=
    □ ∀ π (map : gmap string (val * val)),
      subst_map_rel (free_vars e_t ∪ free_vars e_s) map -∗
      subst_map (fst <$> map) e_t ⪯{π, val_rel} subst_map (snd <$> map) e_s {{ val_rel π }}.

It would seem rather strange to me if expr_rel would make use of weak_val_rel... that indicates we are not following the usual naming scheme.

[Michael Sammler]

I understand that point, but my main problem is that I don't know how to name the other relation if we use val_rel as you suggest. If we find a good name for the other relation, I am fine with using val_rel as you suggest. The name should be a short and easy to understand name as it occurs in many lemmas. I don't like val_rel_nosync because I don't think that the nosync postfix explains much. val_rel_nothreadid would be better in that regard but is quite long. Also the other relation is what really does the relating of values so maybe we should call it real_val_rel? Or raw_val_rel? Or v_rel? My favourite would be raw_val_rel. What do you think or do you have other suggestions?

[Ralf Jung]

From your proposals, I prefer raw_val_rel -- but "raw" is a kind of meaningless prefix (but then so is "weak"^^). Other ideas:

• pre_val_rel/val_rel_pre (another meaningless prefix^^)
• val_rel_obj (the "objective" part of the value relation, which is GPFSL terminology for 'does not depend on the thread')

[Michael Sammler]

I like val_rel_obj or obj_val_rel. Any preference between the two?

[Ralf Jung]

I think I prefer val_rel_obj as this is primarily about values, not about being objective.

Please leave a comment explaining what the "obj" means. :) (I often see abbreviations that are not explained, and then puzzle about what they mean.^^)