[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
PLIB
using PLIB-preds,
filter-count
variables
vm : L → V;
pm : L → V;
h : List((RWevent, Bool));
v : V;
iv : V;
ov : V;
l : L;
il : L;
t : T;
tid : T;
vpe : (RWevent, Bool);
m : Nat;
n : Nat;
e : RWevent;
b : Bool;
state variables
vm : L → V;
pm : L → V;
h : List((RWevent, Bool));
local state variables
t : T;
il : L;
iv : V;
ov : V;
thread id t;
external labels
idle,
ready,
crashed,
invWrite,
resWrite,
invRead,
resRead;
special actions
ADoRead(. .t : T) |
ADoWrite(. .t : T) |
AInvRead(. .t : T;. .l : L) |
AInvWrite(. .t : T;. .loc : L;. .val : V) |
ARetRead(. .t : T;. .v : V) |
ARetWrite(. .t : T);
initial state
vm = ∅ ∧ pm = ∅ ∧ pcf = (λ t. idle) ∧ h = []
declarations
ACrash:
ACrash(pm; vm, h, pcf)
global
{
pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true
}
;
APersist:
APersist(l; pm, h)
global
precondition firstVolWrite(l, h) < # h;
{
let n = firstVolWrite(l, h) in pm(l) := h[n]._1.v, h := h.take(n) + ((h[n]._1, true) + persistDependentReads(l, h.drop(n + 1)))
}
;
TSync:
ready :- TSync(t, h)
atomic
precondition (h | t) | false = [];
{
return ready :-
}
;
ARun:
idle :- ARun()
atomic
{
return ready :-
}
;
INVWRITE:
ready :- INVWRITE(l, v; il, iv)
atomic with AInvWrite(t, l, v)
{
il := l, iv := v; return invWrite :-
}
;
DOWRITE:
invWrite :- DOWRITE(t, il, iv; vm, h)
atomic with ADoWrite(t)
precondition (h | t) | false = [];
{
vm(il) := iv, h := h + (W(t, il, iv), false); return resWrite :-
}
;
RETWRITE:
resWrite :- RETWRITE()
atomic with ARetWrite(t)
{
return ready :-
}
;
assertions
resWrite : (h | t) | false = [] ∨ (h | t) | false = (W(t, il, iv), false) ';
declarations
INVREAD:
ready :- INVREAD(l; il)
atomic with AInvRead(t, l)
{
il := l; return invRead :-
}
;
ADOREAD:
invRead :- ADOREAD(t, il, vm; ov, h)
atomic with ADoRead(t)
{
ov := vm(il), h := h + (R(t, il, vm(il)), h.lastPersistedOrElse(il, true)); return resRead :-
}
;
ARETREAD:
resRead :- ARETREAD(ov; v)
atomic with ARetRead(t, v)
{
v := ov; return ready :-
}
;
assertions
: allReadsOK(h);
: allWritesOK(h);
: vm = ∅ ⊕ h;
: pm = ∅ ⊕ (h | true);
rely condition
rely(t, h, h0);
end automaton specification ;;; END
------------------------------------------------
base =
enrich
PLIB-preds,
filter-count
with
variables
vm : L → V;
pm : L → V;
h : List((RWevent, Bool));
v : V;
iv : V;
ov : V;
l : L;
il : L;
t : T;
tid : T;
vpe : (RWevent, Bool);
m : Nat;
n : Nat;
e : RWevent;
b : Bool;
end enrich
pc =
data specification
PLIBPC = crashed
| idle
| invRead
| invWrite
| ready
| resRead
| resWrite
;
variables
pc : PLIBPC;
end data specification
gs =
data specification
using base
PLIBGState := mkPLIBgs(. .vm : L → V;. .pm : L → V;. .h : List((RWevent, Bool)))
;
variables
gs : PLIBGState;
vm : L → V;
pm : L → V;
h : List((RWevent, Bool));
end data specification
ls =
data specification
using base
PLIBLState := mkPLIBls(. .t : T;. .il : L;. .iv : V;. .ov : V)
;
variables
ls : PLIBLState;
t : T;
il : L;
iv : V;
ov : V;
end data specification
state =
data specification
using pc, localstate,
globalstate
PLIBState := mkstate(. .gstate : PLIBGState;. .lsf : T → PLIBLState;. .pcf : T → PLIBPC)
;
variables
s : PLIBState;
lsf : T → PLIBLState;
pcf : T → PLIBPC;
gstate : PLIBGState;
end data specification
action =
data specification
using base
data types
PLIBAction = ADoRead(. .t : T)
| ADoWrite(. .t : T)
| AInvRead(. .t : T;. .l : L)
| AInvWrite(. .t : T;. .loc : L;. .val : V)
| ARetRead(. .t : T;. .v : V)
| ARetWrite(. .t : T)
| callARun(. .t : T)
| callTSync(. .t : T)
| globalACrash
| globalAPersist(. .invAPersistl : L)
| τ
;
variables
a : PLIBAction;
t : T;
l : L;
loc : L;
val : V;
v : V;
invAPersistl : L;
end data specification
step =
enrich
state,
action
with
functions
lstepf : PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBLState;
gstepf : PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBGState;
pcstepf : PLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBPC;
predicates
PLIBRely : PLIBGState × T × PLIBGState;
plibInit : PLIBState;
plibStep : PLIBState × PLIBAction × PLIBState;
pre : PLIBGState × PLIBLState × PLIBPC × PLIBAction;
lstep : PLIBGState × PLIBLState × PLIBPC × PLIBAction × PLIBGState × PLIBLState × PLIBPC;
PLIBGInv : PLIBGState;
PLIBLInv : PLIBGState × PLIBLState × PLIBPC;
PLIBInv : PLIBGState × (T → PLIBLState) × (T → PLIBPC);
procedures ACrash (L → V) : (L → V) × List((RWevent, Bool)) × (T → PLIBPC) nonfunctional ;
APersist L : (L → V) × List((RWevent, Bool)) nonfunctional ;
TSync T × List((RWevent, Bool)) : ;
ARun : ;
INVWRITE L × V : L × V nonfunctional ;
DOWRITE T × L × V : (L → V) × List((RWevent, Bool)) nonfunctional ;
RETWRITE : ;
INVREAD L : L nonfunctional ;
ADOREAD T × L × (L → V) : V × List((RWevent, Bool)) nonfunctional ;
ARETREAD V : : V ;
axioms
PLIBInv: PLIBInv(gs, lsf, pcf) ↔ PLIBGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), pcf(t)));
PLIBGInv: PLIBGInv(gs) ↔ allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true);
PLIBLInv: PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) ';
plibInit: plibInit(mkstate(gs, lsf, pcf)) ↔ (gs.vm = ∅ ∧ gs.pm = ∅ ∧ pcf = (λ t. idle) ∧ gs.h = []) ∧ (∀ t. lsf(t).t = t);
plibStep:
plibStep(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))
∨ a = globalACrash
∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)
∨ (∃ l.
a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h
∧ gs0
= (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v))
.h:= ( gs.h.take(firstVolWrite(l, gs.h))
+ ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1))))
∧ 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-idle: pre(gs, ls, idle, a) ↔ a = callARun(ls.t);
used for: s, ls;
pre-invRead: pre(gs, ls, invRead, a) ↔ a = ADoRead(ls.t);
used for: s, ls;
pre-invWrite: pre(gs, ls, invWrite, a) ↔ a = ADoWrite(ls.t) ∧ (gs.h | ls.t) | false = [];
used for: s, ls;
pre-ready:
pre(gs, ls, ready, a) ↔ a = callTSync(ls.t) ∧ (gs.h | ls.t) | false = [] ∨ (∃ l, v. a = AInvWrite(ls.t, l, v)) ∨ (∃ l. a = AInvRead(ls.t, l));
used for: s, ls;
pre-resRead: pre(gs, ls, resRead, a) ↔ (∃ v0. a = ARetRead(ls.t, v0) ∧ v0 = ls.ov);
used for: s, ls;
pre-resWrite: pre(gs, ls, resWrite, a) ↔ a = ARetWrite(ls.t);
used for: s, ls;
pre-crashed: pre(gs, ls, crashed, a) ↔ false;
used for: s, ls;
lstepf-ready-TSync: ls.t = t → lstepf(gs, ls, ready, callTSync(t)) = ls;
used for: s, ls;
lstepf-idle-ARun: ls.t = t → lstepf(gs, ls, idle, callARun(t)) = ls;
used for: s, ls;
lstepf-ready-INVWRITE: ls.t = t → lstepf(gs, ls, ready, AInvWrite(t, l, v)) = (ls.il:= l).iv:= v;
used for: s, ls;
lstepf-invWrite-DOWRITE: ls.t = t → lstepf(gs, ls, invWrite, ADoWrite(t)) = ls;
used for: s, ls;
lstepf-resWrite-RETWRITE: ls.t = t → lstepf(gs, ls, resWrite, ARetWrite(t)) = ls;
used for: s, ls;
lstepf-ready-INVREAD: ls.t = t → lstepf(gs, ls, ready, AInvRead(t, l)) = ls.il:= l;
used for: s, ls;
lstepf-invRead-ADOREAD: ls.t = t → lstepf(gs, ls, invRead, ADoRead(t)) = ls.ov:= gs.vm(ls.il);
used for: s, ls;
lstepf-resRead-ARETREAD: ls.t = t → lstepf(gs, ls, resRead, ARetRead(t, v0)) = ls;
used for: s, ls;
gstepf-idle-ARun: ls.t = t → gstepf(gs, ls, idle, callARun(t)) = gs;
used for: s, ls;
gstepf-invRead-ADOREAD:
ls.t = t → gstepf(gs, ls, invRead, ADoRead(t)) = gs.h:= (gs.h + (R(ls.t, ls.il, gs.vm(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)));
used for: s, ls;
gstepf-invWrite-DOWRITE:
ls.t = t → gstepf(gs, ls, invWrite, ADoWrite(t)) = (gs.vm:= gs.vm(ls.il := ls.iv)).h:= (gs.h + (W(ls.t, ls.il, ls.iv), false));
used for: s, ls;
gstepf-ready: gstepf(gs, ls, ready, a) = gs;
used for: s, ls;
gstepf-resRead-ARETREAD: ls.t = t → gstepf(gs, ls, resRead, ARetRead(t, v0)) = gs;
used for: s, ls;
gstepf-resWrite-RETWRITE: ls.t = t → gstepf(gs, ls, resWrite, ARetWrite(t)) = gs;
used for: s, ls;
pcstepf-ready-TSync: ls.t = t → pcstepf(gs, ls, ready, callTSync(t)) = ready;
used for: s, ls;
pcstepf-idle-ARun: ls.t = t → pcstepf(gs, ls, idle, callARun(t)) = ready;
used for: s, ls;
pcstepf-ready-INVWRITE: ls.t = t → pcstepf(gs, ls, ready, AInvWrite(t, l, v)) = invWrite;
used for: s, ls;
pcstepf-invWrite-DOWRITE: ls.t = t → pcstepf(gs, ls, invWrite, ADoWrite(t)) = resWrite;
used for: s, ls;
pcstepf-resWrite-RETWRITE: ls.t = t → pcstepf(gs, ls, resWrite, ARetWrite(t)) = ready;
used for: s, ls;
pcstepf-ready-INVREAD: ls.t = t → pcstepf(gs, ls, ready, AInvRead(t, l)) = invRead;
used for: s, ls;
pcstepf-invRead-ADOREAD: ls.t = t → pcstepf(gs, ls, invRead, ADoRead(t)) = resRead;
used for: s, ls;
pcstepf-resRead-ARETREAD: ls.t = t → pcstepf(gs, ls, resRead, ARetRead(t, v0)) = ready;
used for: s, ls;
PLIBRely: PLIBRely(gs, t, gs0) ↔ rely(t, gs.h, gs0.h);
end enrich