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).
Merge request reports
Activity
- Resolved by Michael Sammler
Our \Omega is always the same... so maybe this is a good opportunity to make it fixed, instead of adding more syntactic noise everywhere? ;)
27 27 )%E. 28 28 29 29 Lemma remove_store_and_load_sim π: 30 ⊢ sim_ectx val_rel π remove_store_and_load_opt remove_store_and_load val_rel. 30 ⊢ sim_ectx (const val_rel) π remove_store_and_load_opt remove_store_and_load val_rel. On my branch,
val_rel
still has typeval → val → PROP
. I use that to defineweak_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 needsval_rel
instead ofweak_val_rel
. (E.g. the values in the heap bijection are related withval_rel
, notweak_val_rel
.)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 aweak_val_rel
instead ofconst val_rel
on my branch, so there is already a separate definition. Note that bothweak_val_rel
andval_rel
are visible outside of the state interpretation andval_rel
is probably used more often (weak_val_rel
is only really relevant for the calls).weak_val_rel
should probably be named differently, maybeext_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
.Edited by Ralf JungThe 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 calledval_rel
.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?
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 calledval_rel_nosync
(andweak_col
should probably also havesync
somewhere in its name)?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 ofval_rel
to already be what everyone needs.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 ofweak_val_rel
... that indicates we are not following the usual naming scheme.Edited by Ralf JungI 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 usingval_rel
as you suggest. The name should be a short and easy to understand name as it occurs in many lemmas. I don't likeval_rel_nosync
because I don't think that thenosync
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 itreal_val_rel
? Orraw_val_rel
? Orv_rel
? My favourite would beraw_val_rel
. What do you think or do you have other suggestions?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')
Edited by Ralf Jung-
25 25 (D: gmap nat nat) 26 26 (i j k: nat) 27 27 (σ_s σ_t σ : state Λ) 28 (Ω: val Λ → val Λ → PROP). 28 (Ω: thread_id → val Λ → val Λ → PROP). - Resolved by Michael Sammler
added 34 commits
-
cc845f36...c5db9733 - 33 commits from branch
master
- a1f6b809 - Parametrize Omega by the thread_id
-
cc845f36...c5db9733 - 33 commits from branch
Closing in favor of !4 (merged).