[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
using VerifyThis3-sequential,
tidset-npset
comment: This specification defines CMULT, which is run by all threads in alltids concurrently.
The initial sparse array spmx is stored initially in gspmx. Its intended number of rows is r.
The threads pick some arbitrary, nonempty part lspmx (atomically) of gspmx (deleting it from there) and processes it.;
constants alltids : Tidset;
comment: the available thread ids are a finite, nonempty set.;
variables spmx : sparsearray;
lspmx : sparsearray;
gspmx : sparsearray;
x : vector;
y : vector;
ghostlspmxf : Tid → sparsearray;
comment: ghost variable that recods the state of local value lspmx;
tid : Tid;
np : natpair;
r : nat;
axioms alltids-nonempty : ⊦ alltids ≠ ∅;
used for: s, ls;
alltids-all : ⊦ tid ∈ alltids;
used for: s, ls;
state variables spmx : sparsearray;
gspmx : sparsearray;
r : nat;
x : vector;
y : vector;
ghostlspmxf : Tid → sparsearray;
thread id tid : Tid;
initial state gspmx = spmx ∧ y = mkvector(r) ∧ okspmx(spmx, r, # x) ∧ (∀ tid. ghostlspmxf(tid) = ∅)
declarations CMULT:
I :- CMULT#(; tid, gspmx, x, y, ghostlspmxf)
{ {
L1 :-
while gspmx ≠ ∅
do
L2 :- choose* lspmx
with lspmx ≠ ∅ ∧ lspmx ⊆ gspmx
in {gspmx := gspmx \ dom lspmx, ghostlspmxf(tid) := lspmx;
L3 :- while lspmx ≠ ∅
do
L4 :-/* lspmx ≠ ∅ */
choose np
with np ∈ lspmx
in
L5 :-/* np ∈ lspmx */
let val = y[np.r]
in
L6 :-/* np ∈ lspmx */
if* val = y[np.r]
then {y[np.r] := val + lspmx[np] * x[np.c], ghostlspmxf(tid) := ghostlspmxf(tid) -- np;
L7 :- lspmx := lspmx -- np}
ifnone
L0 :- skip}
ifnone skip;
L8:- return F}
}
invariants
: alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), gspmx)
∧ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x
∧ U(alltids, ghostlspmxf) ∪ gspmx ⊆ spmx ∧ # y = r ∧ okspmx(spmx, r, # x)
;
L8, F : gspmx = ∅;
L3, L4, L5, L6 : ghostlspmxf(tid) = lspmx;
L7 : np ∈ lspmx ∧ ghostlspmxf(tid) = lspmx -- np;
I, L1, L2, L8, F : ghostlspmxf(tid) = ∅;
L0 : false;
rely condition ghostlspmxf(tid) = ghostlspmxf0(tid) ∧ gspmx0 ⊆ gspmx;
end automaton specification
------------------------------------------------
base =
enrich
VerifyThis3-sequential,
tidset-npset
with
constants alltids : Tidset;
comment: the available thread ids are a finite, nonempty set.;
variables spmx : sparsearray;
lspmx : sparsearray;
gspmx : sparsearray;
x : vector;
y : vector;
ghostlspmxf : Tid → sparsearray;
comment: ghost variable that recods the state of local value lspmx;
tid : Tid;
np : natpair;
r : nat;
axioms alltids-nonempty : ⊦ alltids ≠ ∅;
used for: s, ls;
alltids-all : ⊦ tid ∈ alltids;
used for: s, ls;
end enrich
pc =
data specification
VF3concPC = I
| F
| L8
| L1
| L5
| L4
| L6
| L3
| L7
| L2
| L0
;
variables pc : VF3concPC;
end data specification
gs =
data specification
using ** SOME SPEC **
VF3concGState := mkgs(. .spmx : sparsearray;
. .gspmx : sparsearray;
. .r : nat;
. .x : vector;
. .y : vector;
. .ghostlspmxf : Tid → sparsearray)
;
variables gs : VF3concGState;
spmx : sparsearray;
gspmx : sparsearray;
r : nat;
x : vector;
y : vector;
ghostlspmxf : Tid → sparsearray;
end data specification
ls =
data specification
using ** SOME SPEC **
VF3concLState := mkls(. .tid : Tid;. .lspmx : sparsearray;. .np : natpair;. .val : elem)
;
variables ls : VF3concLState;
tid : Tid;
lspmx : sparsearray;
np : natpair;
val : elem;
end data specification
state =
data specification
using ** SOME SPEC **, ** SOME SPEC **, ** SOME SPEC **
VF3concState := mkstate(. .gstate : VF3concGState;. .lsf : Tid → VF3concLState;. .pcf : Tid → VF3concPC)
;
variables s : VF3concState;
lsf : Tid → VF3concLState;
pcf : Tid → VF3concPC;
gstate : VF3concGState;
end data specification
action =
data specification
using ** SOME SPEC **
VF3concAction = τ
| invCMULT#(. .tid : Tid)
| retCMULT#(. .tid : Tid)
| chooseL4(. .np : natpair)
| chooseL2(. .lspmx : sparsearray)
;
variables a : VF3concAction;
tid : Tid;
np : natpair;
lspmx : sparsearray;
end data specification
step =
enrich
** SOME SPEC **,
** SOME SPEC **
with
functions lstepf : VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concLState;
gstepf : VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concGState;
pcstepf : VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concPC;
predicates VF3concRely : VF3concGState × Tid × VF3concGState;
VF3concstep : VF3concState × VF3concAction × VF3concState;
pre : VF3concGState × VF3concLState × VF3concPC × VF3concAction;
lstep : VF3concGState × VF3concLState × VF3concPC × VF3concAction × VF3concGState × VF3concLState × VF3concPC;
VF3concGInv : VF3concGState;
VF3concLInv : VF3concGState × VF3concLState × VF3concPC;
VF3concInv : VF3concGState × (Tid → VF3concLState) × (Tid → VF3concPC);
axioms VF3concInv : ⊦ VF3concInv(gs, lsf, pcf) ↔ VF3concGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ VF3concLInv(gs, lsf(tid), pcf(tid)));
VF3concGInv
: ⊦ VF3concGInv(gs)
↔ alldisjointp(alltids, gs.ghostlspmxf) ∧ disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx)
∧ gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x
∧ U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ∧ # gs.y = gs.r ∧ okspmx(gs.spmx, gs.r, # gs.x);
VF3concLInv
: ⊦ VF3concLInv(gs, ls, pc)
↔ (pc = L8 ∨ pc = F → gs.gspmx = ∅) ∧ (pc = L3 ∨ pc = L4 ∨ pc = L5 ∨ pc = L6 → gs.ghostlspmxf(ls.tid) = ls.lspmx)
∧ (pc = L7 → ls.np ∈ ls.lspmx ∧ gs.ghostlspmxf(ls.tid) = ls.lspmx -- ls.np)
∧ (pc = I ∨ pc = L1 ∨ pc = L2 ∨ pc = L8 ∨ pc = F → gs.ghostlspmxf(ls.tid) = ∅) ∧ (pc = L0 → false) ∧ (pc = L8 → true)
∧ (pc = L1 → true) ∧ (pc = L5 → ls.np ∈ ls.lspmx) ∧ (pc = L4 → ls.lspmx ≠ ∅) ∧ (pc = L6 → ls.np ∈ ls.lspmx) ∧ (pc = L3 → true)
∧ (pc = L7 → true) ∧ (pc = L2 → true) ∧ (pc = L0 → true);
VF3concstep
: ⊦ VF3concstep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0))
↔ (∃ tid, ls, pc. lstep(gs, lsf(tid), pcf(tid), a, gs0, ls, pc) ∧ lsf0 = lsf(tid; ls) ∧ pcf0 = pcf(tid; pc));
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-L1 : ⊦ pre(gs, ls, L1, a) ↔ a = τ;
used for: s, ls;
lstepf-L1 : ⊦ lstepf(gs, ls, L1, τ) = ls;
used for: s, ls;
gstepf-L1 : ⊦ gstepf(gs, ls, L1, τ) = gs;
used for: s, ls;
pcstepf-L1 : ⊦ pcstepf(gs, ls, L1, a) = (gs.gspmx ≠ ∅ ⊃ L2;L8);
used for: s, ls;
pre-L2
: ⊦ pre(gs, ls, L2, a)
↔ (∃ lspmx0. (lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) ∧ a = chooseL2(lspmx0)) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx);
used for: s, ls;
lstepf-L2-0 : ⊦ lstepf(gs, ls, L2, τ) = ls;
used for: s, ls;
lstepf-L2-1 : ⊦ lstepf(gs, ls, L2, chooseL2(lspmx0)) = ls.lspmx:= lspmx0;
used for: s, ls;
gstepf-L2-0 : ⊦ gstepf(gs, ls, L2, τ) = gs;
used for: s, ls;
gstepf-L2-1
: ⊦ gstepf(gs, ls, L2, chooseL2(lspmx0))
= (gs.gspmx:= (gs.gspmx \ dom (ls.lspmx:= lspmx0).lspmx))
.ghostlspmxf:= gs.ghostlspmxf((ls.lspmx:= lspmx0).tid; (ls.lspmx:= lspmx0).lspmx);
used for: s, ls;
pcstepf-L2 : ⊦ pcstepf(gs, ls, L2, a) = (∃ lspmx0. a = chooseL2(lspmx0) ⊃ L3;L1);
used for: s, ls;
pre-L3 : ⊦ pre(gs, ls, L3, a) ↔ a = τ;
used for: s, ls;
lstepf-L3 : ⊦ lstepf(gs, ls, L3, τ) = ls;
used for: s, ls;
gstepf-L3 : ⊦ gstepf(gs, ls, L3, τ) = gs;
used for: s, ls;
pcstepf-L3 : ⊦ pcstepf(gs, ls, L3, a) = (ls.lspmx ≠ ∅ ⊃ L4;L1);
used for: s, ls;
pre-L4 : ⊦ pre(gs, ls, L4, a) ↔ (∃ np0. np0 ∈ ls.lspmx ∧ a = chooseL4(np0)) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx);
used for: s, ls;
lstepf-L4-0 : ⊦ lstepf(gs, ls, L4, chooseL4(np0)) = ls.np:= np0;
used for: s, ls;
lstepf-L4-1 : ⊦ lstepf(gs, ls, L4, τ) = ls;
used for: s, ls;
gstepf-L4 : ⊦ gstepf(gs, ls, L4, a) = gs;
used for: s, ls;
pcstepf-L4 : ⊦ pcstepf(gs, ls, L4, a) = (∃ np0. a = chooseL4(np0) ⊃ L5;L0);
used for: s, ls;
pre-L5 : ⊦ pre(gs, ls, L5, a) ↔ a = τ;
used for: s, ls;
lstepf-L5 : ⊦ lstepf(gs, ls, L5, τ) = ls.val:= gs.y[ls.np.r];
used for: s, ls;
gstepf-L5 : ⊦ gstepf(gs, ls, L5, τ) = gs;
used for: s, ls;
pcstepf-L5 : ⊦ pcstepf(gs, ls, L5, a) = L6;
used for: s, ls;
pre-L6 : ⊦ pre(gs, ls, L6, a) ↔ a = τ;
used for: s, ls;
lstepf-L6 : ⊦ lstepf(gs, ls, L6, a) = ls;
used for: s, ls;
gstepf-L6
: ⊦ gstepf(gs, ls, L6, a)
= (ls.val = gs.y[ls.np.r]
⊃ (gs.y:= gs.y[ls.np.r, ls.val + ls.lspmx[ls.np] * gs.x[ls.np.c]])
.ghostlspmxf:= gs.ghostlspmxf(ls.tid; gs.ghostlspmxf(ls.tid) -- ls.np)
;gs
);
used for: s, ls;
pcstepf-L6 : ⊦ pcstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ L7;L3);
used for: s, ls;
pre-L7 : ⊦ pre(gs, ls, L7, a) ↔ a = τ;
used for: s, ls;
lstepf-L7 : ⊦ lstepf(gs, ls, L7, τ) = ls.lspmx:= (ls.lspmx -- ls.np);
used for: s, ls;
gstepf-L7 : ⊦ gstepf(gs, ls, L7, τ) = gs;
used for: s, ls;
pcstepf-L7 : ⊦ pcstepf(gs, ls, L7, a) = L3;
used for: s, ls;
pre-L0 : ⊦ pre(gs, ls, L0, a) ↔ a = τ;
used for: s, ls;
lstepf-L0 : ⊦ lstepf(gs, ls, L0, τ) = ls;
used for: s, ls;
gstepf-L0 : ⊦ gstepf(gs, ls, L0, τ) = gs;
used for: s, ls;
pcstepf-L0 : ⊦ pcstepf(gs, ls, L0, a) = L3;
used for: s, ls;
pre-L8 : ⊦ pre(gs, ls, L8, a) ↔ a = retCMULT#(ls.tid);
used for: s, ls;
lstepf-L8 : ⊦ lstepf(gs, ls, L8, retCMULT#(ls.tid)) = ls;
used for: s, ls;
gstepf-L8 : ⊦ gstepf(gs, ls, L8, retCMULT#(ls.tid)) = gs;
used for: s, ls;
pcstepf-L8 : ⊦ pcstepf(gs, ls, L8, a) = F;
used for: s, ls;
pre-I : ⊦ pre(gs, ls, I, a) ↔ a = invCMULT#(ls.tid);
used for: s, ls;
gstepf-I : ⊦ gstepf(gs, ls, I, a) = gs;
used for: s, ls;
lstepf-I-CMULT : ⊦ lstepf(gs, ls, I, invCMULT#(ls.tid)) = ls;
used for: s, ls;
pcstepf-I-CMULT : ⊦ pcstepf(gs, ls, I, invCMULT#(ls.tid)) = L1;
used for: s, ls;
VF3concRely : ⊦ VF3concRely(gs, tid, gs0) ↔ gs.ghostlspmxf(tid) = gs0.ghostlspmxf(tid) ∧ gs0.gspmx ⊆ gs.gspmx;
end enrich