[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
automaton specification
FLITPSC
using FLITPSCweak-preds
variables
glb : Nat;
loc : Nat;
l : L;
wl : L;
v : V;
mem : L → V;
ctr : L → Nat;
t : T;
p : L → List(FOW);
plin : L → List(FOW);
fowl : List(FOW);
fow : FOW;
writers : L → Set(T);
readers : L → Set(T);
ts : Set(T);
state variables
mem : L → V;
p : L → List(FOW);
ctr : L → Nat;
local state variables
t : T;
ghost variables
writers : L → Set(T);
readers : L → Set(T);
thread id t;
external labels
idle,
ready,
crashed;
special actions
ctrDecPSC(. .tid : T;. .l : L) |
ctrIncPSC(. .tid : T;. .l : L) |
ctrReadPSC(. .tid : T;. .l : L;. .n : Nat) |
doReadPSC(. .tid : T;. .l : L;. .v : V) |
doWritePSC(. .tid : T;. .l : L;. .v : V) |
pwbPSC(. .tid : T;. .l : L) |
sfencePSC(. .tid : T);
initial state
mem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ p = (λ l. []) ∧ ctr = (λ l. 0) ∧ readers = (λ l. ∅) ∧ writers = (λ l. ∅)
declarations
PSCRUN:
idle :- PSCRUN()
atomic
{
return ready :-
}
;
FLITPSCWRITE:
ready :- FLITPSCWRITE(l, v, t; p, ctr, writers)
{
W1 with sfencePSC(t) :-
atomic (∀ l. ¬ FO(t) ∈ p(l)) { skip };
W2 with ctrIncPSC(t, l) :-
ctr(l) := ctr(l) + 1, writers(l) := writers(l) ++ t;
W3 with doWritePSC(t, l, v) :-
p(l) := p(l) + W(v, t);
W4 with pwbPSC(t, l) :-
p(l) := p(l) + FO(t);
W5 with sfencePSC(t) :-
atomic (∀ l. ¬ FO(t) ∈ p(l)) { skip };
W6 with ctrDecPSC(t, l) :-
ctr(l) := ctr(l) - 1, writers(l) := writers(l) -- t;
W7 :- return ready :-
}
;
assertions
W1 -> W7 : notMember(t, readers);
W1 -> W2, W7 : notMember(t, writers);
W3 -> W6 : oneMember(t, l, writers);
W1 -> W2 : noPendingW(t, p);
W2, W3, W6, W7 : noPending(t, p);
W4, W5 : onePendingW(t, l, p);
W5 : FOFollowsW(t, p(l));
declarations
FLITPSCREAD:
ready :- FLITPSCREAD(l, t, mem, ctr; p, readers; v)
{
R1 with doReadPSC(t, l, ((mem ⊕ p))(l)) :-
v := ((mem ⊕ p))(l), readers(l) := readers(l) ++ t;
R2 with ctrReadPSC(t, l, ctr(l)) :-
if* ctr(l) ≠ 0
then {skip;
R3 with pwbPSC(t, l) :-
p(l) := p(l) + FO(t), readers(l) := readers(l) -- t}
else readers(l) := readers(l) -- t;
R4 :- return ready :-
}
;
assertions
R1 -> R4 : notMember(t, writers);
R1, R4 : notMember(t, readers);
R2, R3 : oneMember(t, l, readers);
R1 -> R4 : noPendingW(t, p);
declarations
PSCPERSIST_W:
PSCPERSIST_W(l; mem, p)
global
precondition firstPersistW(p(l)) < # p(l);
{
let n = firstPersistW(p(l)) in mem(l) := p(l)[n].val, p(l) := p(l) -p n
}
;
PSCPERSIST_FO:
PSCPERSIST_FO(l; p)
global
precondition ∃ n. isPersistFO(n, p(l));
{
choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip
}
;
PSCCOMPLETE:
ready :- PSCCOMPLETE(t, p)
atomic
precondition ∀ l. ¬ FO(t) ∈ p(l);
{
return ready :-
}
;
PSCCRASH:
PSCCRASH(; p, ctr, writers, readers, pcf)
global
{
pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅
}
;
assertions
: ctrok(ctr, writers);
: writersOk(p, writers);
: pendingOk(p);
idle, ready : notMember(t, writers);
idle, ready : notMember(t, readers);
idle, ready : noPendingW(t, p);
idle : noPending(t, p);
rely condition
relyws(t, readers, readers0) ∧ relyws(t, writers, writers0) ∧ rely(t, p, p0);
end automaton specification ;;; END
------------------------------------------------
base =
enrich
FLITPSCweak-preds
with
variables
glb : Nat;
loc : Nat;
l : L;
wl : L;
v : V;
mem : L → V;
ctr : L → Nat;
t : T;
p : L → List(FOW);
plin : L → List(FOW);
fowl : List(FOW);
fow : FOW;
writers : L → Set(T);
readers : L → Set(T);
ts : Set(T);
end enrich
pc =
data specification
FLITPSCPC = R1
| R2
| R3
| R4
| W1
| W2
| W3
| W4
| W5
| W6
| W7
| crashed
| idle
| ready
;
variables
pc : FLITPSCPC;
end data specification
gs =
data specification
using base
FLITPSCGState := mkFLITPSCgs(. .mem : L → V;
. .p : L → List(FOW);
. .ctr : L → Nat;
. .writers : L → Set(T);
. .readers : L → Set(T))
;
variables
gs : FLITPSCGState;
mem : L → V;
p : L → List(FOW);
ctr : L → Nat;
writers : L → Set(T);
readers : L → Set(T);
end data specification
ls =
data specification
using base
FLITPSCLState := mkFLITPSCls(. .t : T;. .l : L;. .v : V)
;
variables
ls : FLITPSCLState;
t : T;
l : L;
v : V;
end data specification
state =
data specification
using pc, localstate,
globalstate
FLITPSCState := mkstate(. .gstate : FLITPSCGState;. .lsf : T → FLITPSCLState;. .pcf : T → FLITPSCPC)
;
variables
s : FLITPSCState;
lsf : T → FLITPSCLState;
pcf : T → FLITPSCPC;
gstate : FLITPSCGState;
end data specification
action =
data specification
using base
data types
FLITPSCAction = atomicW1
| atomicW5
| callPSCCOMPLETE(. .t : T)
| callPSCRUN(. .t : T)
| ctrDecPSC(. .tid : T;. .l : L)
| ctrIncPSC(. .tid : T;. .l : L)
| ctrReadPSC(. .tid : T;. .l : L;. .n : Nat)
| doReadPSC(. .tid : T;. .l : L;. .v : V)
| doWritePSC(. .tid : T;. .l : L;. .v : V)
| globalPSCCRASH
| globalPSCPERSIST_FO(. .invPSCPERSIST_FOl : L)
| globalPSCPERSIST_W(. .invPSCPERSIST_Wl : L)
| invFLITPSCREAD(. .t : T;. .invFLITPSCREADl : L)
| invFLITPSCWRITE(. .t : T;. .invFLITPSCWRITEl : L;. .invFLITPSCWRITEv : V)
| pwbPSC(. .tid : T;. .l : L)
| retFLITPSCREAD(. .t : T;. .retFLITPSCREADv : V)
| retFLITPSCWRITE(. .t : T)
| sfencePSC(. .tid : T)
| τ
;
variables
a : FLITPSCAction;
t : T;
tid : T;
l : L;
n : Nat;
v : V;
invPSCPERSIST_FOl : L;
invPSCPERSIST_Wl : L;
invFLITPSCREADl : L;
invFLITPSCWRITEl : L;
invFLITPSCWRITEv : V;
retFLITPSCREADv : V;
end data specification
step =
enrich
state,
action
with
functions
lstepf : FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCLState;
gstepf : FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCGState;
pcstepf : FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction → FLITPSCPC;
predicates
FLITPSCRely : FLITPSCGState × T × FLITPSCGState;
flitpscInit : FLITPSCState;
flitpscStep : FLITPSCState × FLITPSCAction × FLITPSCState;
pre : FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction;
lstep : FLITPSCGState × FLITPSCLState × FLITPSCPC × FLITPSCAction × FLITPSCGState × FLITPSCLState × FLITPSCPC;
FLITPSCGInv : FLITPSCGState;
FLITPSCLInv : FLITPSCGState × FLITPSCLState × FLITPSCPC;
FLITPSCInv : FLITPSCGState × (T → FLITPSCLState) × (T → FLITPSCPC);
procedures PSCRUN : ;
FLITPSCWRITE L × V × T : (L → List(FOW)) × (L → Nat) × (L → Set(T)) nonfunctional ;
FLITPSCREAD L × T × (L → V) × (L → Nat) : (L → List(FOW)) × (L → Set(T)) : V nonfunctional ;
PSCPERSIST_W L : (L → V) × (L → List(FOW)) nonfunctional ;
PSCPERSIST_FO L : (L → List(FOW)) nonfunctional nondeterministic;
PSCCOMPLETE T × (L → List(FOW)) : ;
PSCCRASH : (L → List(FOW)) × (L → Nat) × (L → Set(T)) × (L → Set(T)) × (T → FLITPSCPC) nonfunctional ;
axioms
FLITPSCInv: FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)));
FLITPSCGInv: FLITPSCGInv(gs) ↔ ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p);
FLITPSCLInv:
FLITPSCLInv(gs, ls, pc)
↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers))
∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers))
∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p))
∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l)))
∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers))
∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p))
∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers))
∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p));
flitpscInit:
flitpscInit(mkstate(gs, lsf, pcf))
↔ (gs.mem = (λ l. O) ∧ pcf = (λ tid. idle) ∧ gs.p = (λ l. []) ∧ gs.ctr = (λ l. 0) ∧ gs.readers = (λ l. ∅) ∧ gs.writers = (λ l. ∅))
∧ (∀ t. lsf(t).t = t);
flitpscStep:
flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0))
↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc))
∨ (∃ l.
a = globalPSCPERSIST_W(l) ∧ firstPersistW(gs.p(l)) < # gs.p(l)
∧ gs0 = (gs.mem:= gs.mem(l := gs.p(l)[firstPersistW(gs.p(l))].val)).p:= gs.p(l := gs.p(l) -p firstPersistW(gs.p(l))) ∧ lsf0 = lsf
∧ pcf0 = pcf)
∨ (∃ l.
a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs.p(l)))
∧ ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf))
∨ a = globalPSCCRASH
∧ ⟨p := gs.p, ctr := gs.ctr, writers := gs.writers, readers := gs.readers; PSCCRASH(; p, ctr, writers, readers, pcf);
gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf);
lstep:
lstep(gs, ls, pc, a, gs0, ls0, pc0)
↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a);
pre-W1: pre(gs, ls, W1, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t);
used for: s, ls;
pre-W2: pre(gs, ls, W2, a) ↔ a = ctrIncPSC(ls.t, ls.l);
used for: s, ls;
pre-W3: pre(gs, ls, W3, a) ↔ a = doWritePSC(ls.t, ls.l, ls.v);
used for: s, ls;
pre-W4: pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l);
used for: s, ls;
pre-W5: pre(gs, ls, W5, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t);
used for: s, ls;
pre-W6: pre(gs, ls, W6, a) ↔ a = ctrDecPSC(ls.t, ls.l);
used for: s, ls;
pre-W7: pre(gs, ls, W7, a) ↔ a = retFLITPSCWRITE(ls.t);
used for: s, ls;
pre-R1: pre(gs, ls, R1, a) ↔ a = doReadPSC(ls.t, ls.l, ((gs.mem ⊕ gs.p))(ls.l));
used for: s, ls;
pre-R2: pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l));
used for: s, ls;
pre-R3: pre(gs, ls, R3, a) ↔ a = pwbPSC(ls.t, ls.l);
used for: s, ls;
pre-R4: pre(gs, ls, R4, a) ↔ a = retFLITPSCREAD(ls.t, ls.v);
used for: s, ls;
pre-idle: pre(gs, ls, idle, a) ↔ a = callPSCRUN(ls.t);
used for: s, ls;
pre-ready:
pre(gs, ls, ready, a)
↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0))
∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l));
used for: s, ls;
pre-crashed: pre(gs, ls, crashed, a) ↔ false;
used for: s, ls;
lstepf-ready-FLITPSCWRITE: ls.t = t → lstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = (ls.l:= l0).v:= v0;
used for: s, ls;
lstepf-W1: lstepf(gs, ls, W1, a) = ls;
used for: s, ls;
lstepf-W2: lstepf(gs, ls, W2, a) = ls;
used for: s, ls;
lstepf-W3: lstepf(gs, ls, W3, a) = ls;
used for: s, ls;
lstepf-W4: lstepf(gs, ls, W4, a) = ls;
used for: s, ls;
lstepf-W5: lstepf(gs, ls, W5, a) = ls;
used for: s, ls;
lstepf-W6: lstepf(gs, ls, W6, a) = ls;
used for: s, ls;
lstepf-W7: ls.t = t → lstepf(gs, ls, W7, retFLITPSCWRITE(t)) = ls;
used for: s, ls;
lstepf-ready-FLITPSCREAD: ls.t = t → lstepf(gs, ls, ready, invFLITPSCREAD(t, l0)) = ls.l:= l0;
used for: s, ls;
lstepf-R1: lstepf(gs, ls, R1, a) = ls.v:= ((gs.mem ⊕ gs.p))(ls.l);
used for: s, ls;
lstepf-R2: lstepf(gs, ls, R2, a) = ls;
used for: s, ls;
lstepf-R3: lstepf(gs, ls, R3, a) = ls;
used for: s, ls;
lstepf-R4: ls.t = t → lstepf(gs, ls, R4, retFLITPSCREAD(t, ls.v)) = ls;
used for: s, ls;
lstepf-idle-PSCRUN: ls.t = t → lstepf(gs, ls, idle, callPSCRUN(t)) = ls;
used for: s, ls;
lstepf-ready-PSCCOMPLETE: ls.t = t → lstepf(gs, ls, ready, callPSCCOMPLETE(t)) = ls;
used for: s, ls;
gstepf-R1: gstepf(gs, ls, R1, a) = gs.readers:= gs.readers(ls.l := gs.readers(ls.l) ++ ls.t);
used for: s, ls;
gstepf-R2: gstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ gs;gs.readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t));
used for: s, ls;
gstepf-R3: gstepf(gs, ls, R3, a) = (gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t))).readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t);
used for: s, ls;
gstepf-R4: ls.t = t → gstepf(gs, ls, R4, retFLITPSCREAD(t, v)) = gs;
used for: s, ls;
gstepf-W1: gstepf(gs, ls, W1, a) = gs;
used for: s, ls;
gstepf-W2: gstepf(gs, ls, W2, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) + 1)).writers:= gs.writers(ls.l := gs.writers(ls.l) ++ ls.t);
used for: s, ls;
gstepf-W3: gstepf(gs, ls, W3, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + W(ls.v, ls.t));
used for: s, ls;
gstepf-W4: gstepf(gs, ls, W4, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t));
used for: s, ls;
gstepf-W5: gstepf(gs, ls, W5, a) = gs;
used for: s, ls;
gstepf-W6: gstepf(gs, ls, W6, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) - 1)).writers:= gs.writers(ls.l := gs.writers(ls.l) -- ls.t);
used for: s, ls;
gstepf-W7: ls.t = t → gstepf(gs, ls, W7, retFLITPSCWRITE(t)) = gs;
used for: s, ls;
gstepf-idle-PSCRUN: ls.t = t → gstepf(gs, ls, idle, callPSCRUN(t)) = gs;
used for: s, ls;
gstepf-ready: gstepf(gs, ls, ready, a) = gs;
used for: s, ls;
pcstepf-ready-FLITPSCWRITE: ls.t = t → pcstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = W1;
used for: s, ls;
pcstepf-W1: pcstepf(gs, ls, W1, a) = W2;
used for: s, ls;
pcstepf-W2: pcstepf(gs, ls, W2, a) = W3;
used for: s, ls;
pcstepf-W3: pcstepf(gs, ls, W3, a) = W4;
used for: s, ls;
pcstepf-W4: pcstepf(gs, ls, W4, a) = W5;
used for: s, ls;
pcstepf-W5: pcstepf(gs, ls, W5, a) = W6;
used for: s, ls;
pcstepf-W6: pcstepf(gs, ls, W6, a) = W7;
used for: s, ls;
pcstepf-W7: pcstepf(gs, ls, W7, a) = ready;
used for: s, ls;
pcstepf-ready-FLITPSCREAD: ls.t = t → pcstepf(gs, ls, ready, invFLITPSCREAD(t, l0)) = R1;
used for: s, ls;
pcstepf-R1: pcstepf(gs, ls, R1, a) = R2;
used for: s, ls;
pcstepf-R2: pcstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ R3;R4);
used for: s, ls;
pcstepf-R3: pcstepf(gs, ls, R3, a) = R4;
used for: s, ls;
pcstepf-R4: pcstepf(gs, ls, R4, a) = ready;
used for: s, ls;
pcstepf-idle-PSCRUN: ls.t = t → pcstepf(gs, ls, idle, callPSCRUN(t)) = ready;
used for: s, ls;
pcstepf-ready-PSCCOMPLETE: ls.t = t → pcstepf(gs, ls, ready, callPSCCOMPLETE(t)) = ready;
used for: s, ls;
FLITPSCRely: FLITPSCRely(gs, t, gs0) ↔ relyws(t, gs.readers, gs0.readers) ∧ relyws(t, gs.writers, gs0.writers) ∧ rely(t, gs.p, gs0.p);
end enrich