[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,
data asm specification
apersistence
using apersistence-base
procedures apersistence_read_gnd#
address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: group-node
: error
nondeterministic;
apersistence_read_ind#
address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: index-node
: error
nondeterministic;
apersistence_read_gblock_nodes#
nat × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: address-list × group-node-list
: error
nondeterministic;
apersistence_get_gc_block#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: nat
: error
nondeterministic;
apersistence_add_gnds#
group-node-list × address × index-store × index-store × nat-set × group-store × nat-list × nat × nat-set
: address-list × group-store × persistence-state × bool
: error
nondeterministic;
apersistence_add_ind#
index-node × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set
: address × index-store × persistence-state × bool
: error
nondeterministic;
apersistence_is_readonly#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool
;
apersistence_get_leb_size#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool : : nat
;
apersistence_sync#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set : persistence-state × bool : error
nondeterministic;
apersistence_set_gblock_refsize#
nat × nat × address × index-store × index-store × nat-set × group-store × nat-list × nat × nat-set × persistence-state × bool
: group-store
nonfunctional
;
apersistence_set_iblock_refsize#
nat × nat × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: index-store
nonfunctional
;
apersistence_get_gblock_refsize#
nat × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat
;
apersistence_get_iblock_refsize#
nat × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat
;
apersistence_get_block_free_size#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool : : nat
nondeterministic;
apersistence_is_log_empty#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool
;
apersistence_allocate_gnd#
address × index-store × index-store × group-store × nat × nat-set × bool : nat-set × group-store × nat-list × persistence-state : error
nondeterministic;
apersistence_deallocate_gnd#
nat × address × index-store × index-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: nat-set × group-store
: error
nondeterministic;
apersistence_allocate_ind#
address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : index-store × persistence-state : error
nondeterministic;
apersistence_commit#
address × nat × bool
: nat-set × index-store × nat-set × group-store × address × index-store × group-store × nat-list × nat × nat-set
: persistence-state × error
nondeterministic;
apersistence_requires_commit#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool
nondeterministic;
apersistence_format#
nat × nat × nat
:
: address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool ×
error
nondeterministic;
apersistence_recover#
: address × nat × nat-list × nat-set × address × nat-list × nat × nat-set × index-store × index-store × nat-set × group-store ×
group-store
: persistence-state × bool × error
nondeterministic;
variables ADR : address flexible;
LADR : laddress flexible;
NS : nat-set flexible;
NS0 : nat-set flexible;
NS1 : nat-set flexible;
OS : nat-set flexible;
OS0 : nat-set flexible;
GND : group-node flexible;
IND : index-node flexible;
ADRLIST : address-list flexible;
LADRLIST : laddress-list flexible;
GNDLIST : group-node-list flexible;
MAXINO : nat flexible;
MAXINO0 : nat flexible;
LNUM : nat flexible;
N : nat flexible;
N0 : nat flexible;
OFFSET : nat flexible;
GSTORE : group-store flexible;
GSTORE0 : group-store flexible;
GINVAL : nat-set flexible;
ISTORE : index-store flexible;
ISTORE0 : index-store flexible;
NL : nat-list flexible;
NL0 : nat-list flexible;
ERR : error flexible;
ERR0 : error flexible;
ROOTADR : address flexible;
ROOTADR0 : address flexible;
ISGBLOCK : bool flexible;
VOLSIZE : nat flexible;
SIZE : nat flexible;
COMMIT? : bool flexible;
EMPTY? : bool flexible;
PSTATE : persistence-state flexible;
PSYNCED : bool flexible;
ROFS : bool flexible;
state variables ROOTADR : address flexible;
ISTORE : index-store flexible;
ISTORE0 : index-store flexible;
GINVAL : nat-set flexible;
GSTORE : group-store flexible;
GSTORE0 : group-store flexible;
NL : nat-list flexible;
MAXINO : nat flexible;
OS : nat-set flexible;
PSTATE : persistence-state flexible;
PSYNCED : bool flexible;
initialization procedure apersistence_format#
if ERR = ESUCCESS
sequential
invariants journal : ⊦ inv-journal(NL, GSTORE, GSTORE0, GINVAL);
index : ⊦ inv-index(ISTORE, ISTORE0);
state : ⊦ inv-state(PSTATE, NL, GSTORE, ISTORE, PSYNCED);
crash predicate ROOTADR = ROOTADR` ∧ ISTORE = remove-refsize0(crash(ISTORE`, ISTORE0`)) ∧ ISTORE0 = ISTORE0` ∧ GINVAL = GINVAL`
∧ GSTORE = crash(GSTORE`, GSTORE0`, GINVAL`, NL`) ∧ GSTORE0 = GSTORE0` ∧ NL = NL` ∧ MAXINO = MAXINO` ∧ OS = OS`
with crash-neutrality
synchronized predicate
PSYNCED
recovery procedure apersistence_recover#
if ERR = ESUCCESS
declarations read-gnd:
apersistence_read_gnd#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GND; ERR)
precondition ADR ∈ GSTORE ∧ ¬ ADR.lnum ∈ GINVAL;
postcondition true;
{if ADR ∈ GSTORE ∧ ¬ ADR.lnum ∈ GINVAL
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GND := GSTORE[ADR] else GND := ?}
else abort
}
read-ind:
apersistence_read_ind#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; IND; ERR)
precondition ADR ∈ ISTORE;
postcondition true;
{if ADR ∈ ISTORE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then IND := ISTORE[ADR] else IND := ?} else abort
}
read-gblock:
apersistence_read_gblock_nodes#
(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ADRLIST, GNDLIST; ERR)
precondition LNUM ∈ GSTORE ∧ ¬ LNUM ∈ GINVAL;
postcondition true;
{if LNUM ∈ GSTORE ∧ ¬ LNUM ∈ GINVAL
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then ADRLIST := ADRLIST + GSTORE[LNUM].ladrlist.to-adr(LNUM), GNDLIST := GNDLIST + GSTORE[LNUM].gndlist
else ADRLIST := ?, GNDLIST := ?}
else abort
}
get-gc-block:
apersistence_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR)
precondition true;
postcondition true;
{{ERR := ENOSPC or choose N0 with N0 ∈ dom GSTORE ∧ ¬ N0 ∈ NL in {N := N0; ERR := ESUCCESS} ifnone ERR := ENOSPC}
}
add-gnds:
apersistence_add_gnds#(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR)
precondition PSTATE.journal? ∨ PSTATE = readonly;
postcondition true;
{if PSTATE.journal? ∨ PSTATE = readonly
then if PSTATE = readonly
then ERR := EROFS
else {choose LADRLIST, ERR0
with (⌊ERR0⌋ ∨ ERR0 = ESUCCESS) ∧ ¬ dups(GSTORE[PSTATE.lnum].ladrlist + LADRLIST) ∧ # LADRLIST ≤ # GNDLIST
∧ inv-flashsize(prefixn(# LADRLIST, GNDLIST), LADRLIST) ∧ (ERR0 = ESUCCESS ↔ # LADRLIST = # GNDLIST)
in {ADRLIST := LADRLIST.to-adr(PSTATE.lnum), ERR := ERR0;
GSTORE[PSTATE.lnum].gndlist := GSTORE[PSTATE.lnum].gndlist + prefixn(# LADRLIST, GNDLIST);
GSTORE[PSTATE.lnum].ladrlist := GSTORE[PSTATE.lnum].ladrlist + LADRLIST;
if ERR ≠ ESUCCESS then ADRLIST := ?, PSTATE := readonly};
PSYNCED := ?}
else abort
}
add-ind:
apersistence_add_ind#(IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ISTORE, PSTATE, PSYNCED; ERR)
precondition PSTATE.index? ∨ PSTATE = readonly;
postcondition true;
{if PSTATE.index? ∨ PSTATE = readonly
then if PSTATE = readonly
then ERR := EROFS
else {choose OFFSET, ERR0
with ¬ @(PSTATE.lnum, OFFSET, IND.flashsize) ∈ ISTORE ∧ ERR0 = ESUCCESS ∨ ⌊ERR0⌋
in ADR := @(PSTATE.lnum, OFFSET, IND.flashsize), ERR := ERR0;
if ERR = ESUCCESS
then {ISTORE[PSTATE.lnum].indlist := ISTORE[PSTATE.lnum].indlist + IND;
ISTORE[PSTATE.lnum].ladrlist := ISTORE[PSTATE.lnum].ladrlist + @(ADR.pos, ADR.size)}
else ADR := ?, PSTATE := readonly;
PSYNCED := ?}
else abort
}
is-readonly:
apersistence_is_readonly#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; ROFS)
precondition true;
postcondition true;
{ROFS := PSTATE = readonly
}
get-leb-size:
apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition true;
postcondition true;
{N := LEB_SIZE
}
sync:
apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)
precondition true;
postcondition true;
{if PSTATE = readonly
then ERR := EROFS
else if PSTATE = unbuffered
then ERR := ESUCCESS
else {fail_or_success#(; ; ERR); PSYNCED := ERR = ESUCCESS; skip or PSTATE := readonly}
}
set-gblock-refsize:
apersistence_set_gblock_refsize#(LNUM, N, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GSTORE)
precondition LNUM ∈ GSTORE;
postcondition true;
{if LNUM ∈ GSTORE then GSTORE[LNUM].ref-size := N else abort
}
set-iblock-refsize:
apersistence_set_iblock_refsize#(LNUM, N, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)
precondition LNUM ∈ ISTORE;
postcondition true;
{if LNUM ∈ ISTORE then ISTORE[LNUM].ref-size := N else abort
}
get-gblock-refsize:
apersistence_get_gblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition LNUM ∈ GSTORE;
postcondition true;
{if LNUM ∈ GSTORE then N := GSTORE[LNUM].ref-size else abort
}
get-iblock-refsize:
apersistence_get_iblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition LNUM ∈ ISTORE;
postcondition true;
{if LNUM ∈ ISTORE then N := ISTORE[LNUM].ref-size else abort
}
get-block-free-size:
apersistence_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition true;
postcondition true;
{if PSTATE = unbuffered then N := 0 else choose N0 with N0 ≤ LEB_SIZE in N := N0
}
is-log-empty:
apersistence_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?)
precondition true;
postcondition true;
{EMPTY? := NL = []
}
allocate-gnd:
apersistence_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR)
precondition PSYNCED;
postcondition true;
{if PSYNCED
then if PSTATE = readonly
then ERR := EROFS
else {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then choose N
with ¬ N ∈ GSTORE
in GSTORE[N] := groupblock([], [], 0), NL := NL + N, GINVAL := GINVAL -- N, PSTATE := journal(N)}
else abort
}
deallocate-gnd:
apersistence_deallocate_gnd#(N, ROOTADR, ISTORE, ISTORE0, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GINVAL, GSTORE; ERR)
precondition PSYNCED ∧ N ∈ GSTORE ∧ ¬ N ∈ NL;
postcondition true;
{if PSYNCED ∧ N ∈ GSTORE ∧ ¬ N ∈ NL
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GSTORE := GSTORE -- N, GINVAL := GINVAL ++ N}
else abort
}
allocate-ind:
apersistence_allocate_ind#(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR)
precondition PSYNCED;
postcondition true;
{if PSYNCED
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then choose N with ¬ N ∈ ISTORE in ISTORE[N] := indexblock([], [], 0), PSTATE := index(N)}
else abort
}
commit:
apersistence_commit#
(ROOTADR0, MAXINO0, PSYNCED; OS0, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS; PSTATE, ERR)
precondition PSYNCED ∧ dom remove-refsize0(GSTORE) ∩ GINVAL = ∅;
postcondition true;
{if PSYNCED ∧ dom remove-refsize0(GSTORE) ∩ GINVAL = ∅
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {ISTORE := remove-refsize0(ISTORE); ISTORE0 := ISTORE; GSTORE := remove-refsize0(GSTORE); GSTORE0 := GSTORE; GINVAL := ∅;
ROOTADR := ROOTADR0; OS := OS0; NL := []; MAXINO := MAXINO0; PSTATE := unbuffered}
else PSTATE := readonly;
OS0 := ?}
else abort
}
requires-commit:
apersistence_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?)
precondition true;
postcondition true;
{COMMIT? := ?
}
format:
apersistence_format#
(VOLSIZE, SIZE, MAXINO0; ; ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then PSTATE := unbuffered, PSYNCED := true, MAXINO := MAXINO0, OS := ∅, NL := [], GSTORE := ∅, GSTORE0 := ∅, ISTORE := ∅,
ISTORE0 := ∅, GINVAL := ∅, ROOTADR := ?
else PSTATE := ?, PSYNCED := ?, MAXINO := ?, OS := ?, NL := ?, GSTORE := ?, GSTORE0 := ?, ISTORE := ?, ISTORE0 := ?,
GINVAL := ?, ROOTADR := ?}
else abort
}
recovery:
apersistence_recover#
(; ROOTADR0, MAXINO0, NL0, OS0, ROOTADR, NL, MAXINO, OS, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0; PSTATE, PSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then PSTATE := unbuffered, PSYNCED := true, ROOTADR0 := ROOTADR, MAXINO0 := MAXINO, NL0 := NL, OS0 := OS
else PSTATE := ?, PSYNCED := ?, ROOTADR := ?, ISTORE := ?, ISTORE0 := ?, GINVAL := ?, GSTORE := ?, GSTORE0 := ?, NL := ?,
MAXINO := ?, OS := ?, ROOTADR0 := ?, MAXINO0 := ?, NL0 := ?, OS0 := ?}
}
end data asm specification