Thm*  E:EventStruct, P:TraceProperty(E), A:Type, evt:(A  |E|)
, tg:(ALabel), tr_u:Trace(E), tr_l:A List.
switchable(E)(P)  
No-dup-send(E)(tr_u)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u) | [switch_main_theorem] |
|
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, evt:(A|E|), tg:(ALabel)
, tr:A List.
switchable(E)(P)
No-dup-send(E)(map(evt;tr))
switch_inv( < A,evt,tg > (E))(tr) (m:Label. P(map(evt; < tr > _m))) P(map(evt;tr)) | [switch_theorem] |
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, P:((|E| List)Prop), A:Type, f:(A|E|)
, t:(ALabel). switchable(E)(P) switchable( < A,f,t > (E))(P o f) | [switchable_induced_tagged] |
|
Thm* E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop).
switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f) | [switchable_induced] |
Thm* E:EventStruct, tr:|E| List, ls: ||tr||.
is-send(E)(tr[ls])
(j:||tr||. ls < j  is-send(E)(tr[j]))
(i,j:||tr||. i j is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)) | [switch_inv_rel_closure_lemma1] |
|
Thm* E:TaggedEventStruct, tr:|E| List, ls:||tr||.
switch_inv(E)(tr)
(i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j])) | [switch_inv_rel_closure] |
Thm* E:TaggedEventStruct, tr:|E| List.
switch_inv(E)(tr)  (i,j:||tr||. (i switchR(tr) j) tag(E)(tr[i]) = tag(E)(tr[j])) | [switch_inv_rel_same_tag] |
|
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||.
is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i]) | [switch_inv_rel_closure_send] |
Thm* E:EventStruct, P:((Label(|E| List))Prop).
(f,g:(Label(|E| List)). (p:Label. g(p) f(p)) P(f) P(g))
(f,g:(Label(|E| List)).
( a:|E|. p:Label. g(p) = filter( b. (b =msg=(E) a);f(p))) P(f) P(g))
(f,g,h:(Label(|E| List)).
(p,q:Label. (x f(p).(yg(q).(x =msg=(E) y))))
(p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h))
switchable0(E)(local_deliver_property(E;P)) | [local_deliver_switchable] |
|
Thm* E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z) | [decidable__switch_inv_rel] |
|
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:TaggedEventStruct, x:|E| List, i:(||x||-1).
switch_inv(E)(x)
is-send(E)(x[(i+1)])
is-send(E)(x[i])  loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1)) | [switch_inv_swap] |
|
Thm* E:TaggedEventStruct. switch_inv(E) (|E| List)Prop | [switch_inv_wf] |
|
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x) | [R_async_symmetric] |
|
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, x,y:|E| List.
(x delayableR(E) y) (y delayableR(E) x) | [R_delayable_symmetric] |
|
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:EventStruct, a,b,c:|E|, tr:|E| List.
a somewhere delivered before b a somewhere delivered before c c somewhere delivered before b | [delivered_before_somewhere_lemma] |
|
Thm* E:TaggedEventStruct. safetyR(E) preserves AD-normal(E) | [switch_normal_safety] |
|
Thm* E:EventStruct, a,b:|E|, tr:|E| List.
a somewhere delivered before b
(k:||tr||.
a delivered at time k
(k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))) | [not_delivered_before_somewhere] |
|
Thm* E:EventStruct, tr:|E| List, x,y:|E|.
Dec(x somewhere delivered before y) | [decidable__delivered_before_somewhere] |
|
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), m:Label
, tr1,tr2:A List. (tr1 R(tg) tr2) < tr1 > _m = < tr2 > _m A List | [tag_sublist_preserved] |
|
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop).
(P refines (Causal(E) No-dup-deliver(E)))
((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P)
((I No-dup-send(E)) fuses P) | [no_DASH_dup_DASH_fusion] |
|
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop).
(P refines Causal(E))
((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P) | [tag_by_msg_fusion_lemma] |
|
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:Structure, P,Q_1,Q_2:((|E| List)Prop).
(P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2)) | [tr_refines_and] |
|
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] |
|
Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E) | [P_no_dup_composable] |
|
Thm* E:TaggedEventStruct, tr:|E| List, x,y:|E|.
Dec(R_ad_normal(tr)(x,y)) | [decidable__R_ad_normal] |
|
Thm* E:EventStruct, L:|E| List.
L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i])) | [P_causal_non_nil] |
|
Thm* E:TaggedEventStruct, tr:|E| List.
(m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr) | [P_tag_by_msg_lemma] |
|
Thm* E:EventStruct, tr:|E| List.
No-dup-deliver(E)(tr)
(x,y:|E|.
is-send(E)(x)
is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr)) | [P_no_dup_iff] |
|
Thm* E:EventStruct, tr:|E| List.
Causal(E)(tr) (tr':|E| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))) | [P_causal_iff] |
|
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List.
No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l) | [no_dup_send_induced] |
|
Def adR(E) == (delayableR(E) asyncR(E))^* | [R_ad] |
|
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 layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^* | [layer_rel] |
Def asyncR(E)
== swap adjacent[loc(E)(x) = loc(E)(y)
&  (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))] | [R_async] |
|
Def delayableR(E)
== swap adjacent[(x =msg=(E) y)
& (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))] | [R_delayable] |
|
Def R_permutation(E) == swap adjacent[True] | [R_permutation] |
|
Def MCS(E)(P)
== memorylessR(E) preserves P & (ternary) composableR(E) preserves P & safetyR(E) preserves P | [memoryless_composable_safety] |
|
Def switch-decomposable(E)(L)
== L = nil |E| List
(Q:(||L||Prop).
(i:||L||. Dec(Q(i)))
& (i:||L||. Q(i))
& (i:||L||. Q(i) (is-send(E)(L[i])))
& (i,j:||L||. Q(i) Q(j) tag(E)(L[i]) = tag(E)(L[j]))
& (i,j:||L||. Q(i) ij C(Q)(j))) | [switch_decomposable] |
|
Def totalorder(E)(tr)
== p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q)) | [totalorder] |
|
Def TraceProperty(E) == (|E| List)Prop | [trace_property] |
|
Def P refines Q == tr:|E| List. P(tr) Q(tr) | [tr_refines] |
|
Def send-enabledR(E)(L_1,L_2) == x:|E|. (is-send(E)(x)) & L_2 = (L_1 @ [x]) | [R_send_enabled] |
|
Def memorylessR(E)(L_1,L_2)
== a:|E|. L_2 = filter(b.(b =msg=(E) a);L_1) |E| List | [R_memoryless] |
|
Def safetyR(E)(tr_1,tr_2) == tr_2 tr_1 | [R_safety] |
|
Def R_strong_safety(E)(tr_1,tr_2) == sublist(|E|;tr_2;tr_1) | [R_strong_safety] |
|
Def composableR(E)(L_1,L_2,L)
== (xL_1.(yL_2.(x =msg=(E) y))) & L = (L_1 @ L_2) |E| List | [R_composable] |
|
Def single-tag-decomposable(E)(L)
== L = nil |E| List
(L_1,L_2:Trace(E).
L = (L_1 @ L_2) |E| List
& L_2 = nil |E| List
& (xL_1.(yL_2.(x =msg=(E) y)))
& (m:Label. (xL_2.tag(E)(x) = m))) | [single_tag_decomposable] |