Module 9 - Usefulness of Compositionality Result - Definition: Globally Sound Use of Modes
if for every state, the global configuration pairing all single threads with the initial mode mods_0 state ensures a sound use of modes.
A global configuration ensures a sound use of modes if it ensures a globally sound use of modes
and each local configuration associated to the pairs of statement and mode state in the global configuration ensures a locally sound use of modes (cf. Definition, slide 20).
A global configuration ensures a globally sound use of modes if EACH mode state tuple reachable from it has compatible modes (cf. Definition, slide 17).
let S :=
// acq(asm-nowrite, debug) // debug := 0;
// rel(asm-nowrite, debug) // skip
like defined on slide 29.
If I understand correct, the global configuration
<(S, mds_0),(y := x, mds_0), sigma>
does not ensure a globally sound use of modes (for any state sigma),
because the second thread does not guarantee that it does not use the variable debug.
But now let S' :=
// acq(guar-nowrite, debug) // y := x;
Do I see right that also
<(S, mds_0),(S', mds_0), sigma>
does NOT ensure a globally sound use of modes (for any state sigma),
because there is a mode state tuple (mds_1, mds_2) reachable from this global configuration (namely when the first thread performs a step first),
where debug is in mds_1(asm-nowrite) but debug is not in mds_2(guar-nowrite) (i.e. the first thread assumes nowrite but the second does not yet guarantee it)
and hence the mode state tuple does not have compatible modes.
Thus do I conclude right that according to the definition of "ensures a globally sound use of modes" (with the quantification over all reachable state tuples), no multithreaded program that assumes a noread or a nowrite somewhere,
with more then one thread (maybe except for threads where the statement is stop and hence are not further executable), can ensure a globally sound use of modes,
and hence the theorem (slide 22) is not applicable to ensure SIFUM security for those multithreaded programs?