Thm*  E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P)  
asyncR(E) preserves P
delayableR(E) preserves P
(P refines (Causal(E)  No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P) | [switch_inv_theorem] |
|
Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E) | [no_duplicate_send_layer] |
|
Thm* E:TaggedEventStruct. safetyR(E) preserves switch_inv(E) | [switch_inv_safety] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P asyncR(E) preserves P | [permutable_implies_async] |
|
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E) | [no_duplicate_send_async] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P delayableR(E) preserves P | [permutable_implies_delayable] |
|
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E) | [no_duplicate_send_delayable] |
|
Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E) | [P_no_dup_permutable] |
|
Thm* E:TaggedEventStruct, P,I:TraceProperty(E).
MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P) | [M_DASH_C_DASH_S_SPACE_induction] |
|
Thm* E:TaggedEventStruct. safetyR(E) preserves AD-normal(E) | [switch_normal_safety] |
|
Thm* E:TaggedEventStruct. safetyR(E) preserves Tag-by-msg(E) | [P_tag_by_msg_safety] |
|
Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E) | [P_no_dup_deliver_safety] |
Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E)
, R:(Trace(E)  Trace(E)Prop).
tag_splitable(E;R)
(tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1))
R preserves P
R preserves K
(tr:Trace(E). (I K)(tr) ( tr':Trace(E). I(tr') & J(tr') & (tr R tr')))
(((I J) K) fuses P) ((I K) fuses P) | [normal_form_fusion] |
|
Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1)) | [memoryless_remove_msgs] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P memorylessR(E) preserves P | [strong_safety_implies_memoryless] |
|
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P safetyR(E) preserves P | [strong_safety_implies_safety] |
|
Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E) | [P_no_dup_send_enabled] |
|
Thm* E:EventStruct. safetyR(E) preserves Causal(E) | [P_causal_safety] |
|
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E) | [no_duplicate_send_safety] |
|
Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E) | [P_no_dup_strong_safety] |
|
Def switchable(E)(P)
== safetyR(E) preserves P
& memorylessR(E) preserves P
& (ternary) composableR(E) preserves P
& send-enabledR(E) preserves P
& asyncR(E) preserves P
& delayableR(E) preserves P
& (P refines Causal(E))
& (P refines No-dup-deliver(E)) | [b_switchable] |
|
Def switchable0(E)(P)
== safetyR(E) preserves P
& memorylessR(E) preserves P
& (ternary) composableR(E) preserves P
& send-enabledR(E) preserves P
& asyncR(E) preserves P
& delayableR(E) preserves P | [switchable0] |
|
Def MCS(E)(P)
== memorylessR(E) preserves P & (ternary) composableR(E) preserves P & safetyR(E) preserves P | [memoryless_composable_safety] |