[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
index
using apersistence-base
,
index-base, aubifs-inv
procedures index_index_contains#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : bool : error
nondeterministic;
index_index_lookup#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : bool × address : error
nondeterministic;
index_index_store#
key × address × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : address × bool × node-index
nonfunctional
nondeterministic;
index_index_remove#
key × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : address × bool × node-index
nonfunctional
nondeterministic;
index_index_truncate#
key × nat × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : address-set × node-index
nonfunctional
;
index_index_entries#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : stringset : error
nondeterministic;
index_get_leb_size node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : : nat ;
index_read_gnd#
address × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : group-node : error
nondeterministic;
index_read_gblock_nodes#
nat × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool
: address-list × group-node-list
: error
nondeterministic;
index_get_gc_block# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : nat : error
nondeterministic;
index_add_gnds#
group-node-list × node-index × node-index × nat-set × group-store × nat-list × nat × nat-set : address-list × group-store : bool × error
nondeterministic;
index_sync# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set : : bool × error
nondeterministic;
index_set_gblock_refsize#
nat × nat × node-index × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : group-store
nonfunctional
;
index_get_gblock_refsize#
nat × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : : nat
;
index_get_block_free_size# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : : nat
nondeterministic;
index_is_log_empty# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : : bool ;
index_allocate_gnd# node-index × node-index × group-store × nat × nat-set × bool : nat-set × group-store × nat-list : error
nondeterministic;
index_deallocate_gnd# nat × node-index × node-index × group-store × nat-list × nat × nat-set × bool : nat-set × group-store : error
nondeterministic;
index_commit#
nat × node-index × bool : nat-set × nat-set × group-store × node-index × group-store × nat-list × nat × nat-set : error
nondeterministic;
index_requires_commit# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : : bool
nondeterministic;
index_format#
nat × nat × nat : : node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool × error
nondeterministic;
index_recover#
: nat × nat-list × nat-set × node-index × nat-list × nat × nat-set × nat-set × group-store × group-store : node-index × bool × error
nondeterministic;
variables PRI : node-index flexible;
PFI : node-index flexible;
PPMAXINO : nat flexible;
PPMAXINO0 : nat flexible;
PSTORE : group-store flexible;
PSTORE0 : group-store flexible;
PINVAL : nat-set flexible;
PNL : nat-list flexible;
PNL0 : nat-list flexible;
P_OS : nat-set flexible;
P_OS0 : nat-set flexible;
EXISTS : bool flexible;
NAMES : stringset flexible;
KEY : key flexible;
ND : node flexible;
KS : key-set flexible;
AS : address-set flexible;
ADR : address flexible;
OLDADR : address flexible;
LADR : laddress flexible;
NS : nat-set flexible;
NS0 : nat-set flexible;
NS1 : nat-set flexible;
GND : group-node flexible;
IND : index-node flexible;
ADRLIST : address-list flexible;
LADRLIST : laddress-list flexible;
GNDLIST : group-node-list flexible;
PMAXINO : nat flexible;
PMAXINO0 : nat flexible;
LNUM : nat flexible;
N : nat flexible;
N0 : nat flexible;
SIZE : nat flexible;
ERR : error flexible;
ERR0 : error flexible;
VOLSIZE : nat flexible;
COMMIT? : bool flexible;
ISYNCED : bool flexible;
EMPTY? : bool flexible;
state variables PRI : node-index flexible;
PFI : node-index flexible;
PINVAL : nat-set flexible;
PSTORE : group-store flexible;
PSTORE0 : group-store flexible;
PNL : nat-list flexible;
PMAXINO : nat flexible;
P_OS : nat-set flexible;
ISYNCED : bool flexible;
initialization procedure index_format#
if ERR = ESUCCESS
sequential
invariants journal : ⊦ inv-journal(PNL, PSTORE, PSTORE0, PINVAL);
ri-inj : ⊦ ri-inj(PRI);
fi-inj : ⊦ ri-inj(PFI);
crash predicate PINVAL = PINVAL` ∧ PSTORE = crash(PSTORE`, PSTORE0`, PINVAL`, PNL`) ∧ PSTORE0 = PSTORE0` ∧ PNL = PNL` ∧ PMAXINO = PMAXINO`
∧ P_OS = P_OS` ∧ PFI = PFI`
with crash-neutrality
synchronized predicate
ISYNCED
recovery procedure index_recover#
if ERR = ESUCCESS
declarations contains:
index_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then EXISTS := KEY ∈ PRI else EXISTS := ?}
}
lookup:
index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS then {EXISTS := KEY ∈ PRI; if EXISTS then ADR := PRI[KEY] else ADR := ?} else EXISTS := ?, ADR := ?}
}
store:
index_index_store#(KEY, ADR, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI)
precondition ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd);
postcondition true;
{if ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd)
then {EXISTS := KEY ∈ PRI; if EXISTS then OLDADR := PRI[KEY] else OLDADR := ?; PRI[KEY] := ADR}
else abort
}
remove:
index_index_remove#(KEY, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI)
precondition true;
postcondition true;
{{EXISTS := KEY ∈ PRI; if EXISTS then {OLDADR := PRI[KEY]; PRI := PRI -- KEY} else OLDADR := ?}
}
truncate:
index_index_truncate#(KEY, N, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PRI)
precondition true;
postcondition true;
{let KS = datakeys(KEY, N, PRI) in PRI := PRI \ KS, AS := PRI[KS]
}
entries:
index_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then NAMES := dentries(KEY, PRI) else NAMES := ?}
}
get-leb-size:
index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N)
precondition true;
postcondition true;
{N := LEB_SIZE
}
read-gnd:
index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR)
precondition ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL;
postcondition true;
{if ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GND := PSTORE[ADR] else GND := ?}
else abort
}
read-gblock:
index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; ERR)
precondition LNUM ∈ PSTORE ∧ ¬ LNUM ∈ PINVAL;
postcondition true;
{if LNUM ∈ PSTORE ∧ ¬ LNUM ∈ PINVAL
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then ADRLIST := ADRLIST + PSTORE[LNUM].ladrlist.to-adr(LNUM), GNDLIST := GNDLIST + PSTORE[LNUM].gndlist
else ADRLIST := ?, GNDLIST := ?}
else abort
}
get-gc-block:
index_get_gc_block#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; N; ERR)
precondition true;
postcondition true;
{{ERR := ENOSPC or choose N0 with N0 ∈ dom PSTORE ∧ ¬ N0 ∈ PNL in {N := N0; ERR := ESUCCESS} ifnone ERR := ENOSPC}
}
add-gnds:
index_add_gnds#(GNDLIST, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS; ADRLIST, PSTORE; ISYNCED, ERR)
precondition PNL ≠ [];
postcondition true;
{if PNL ≠ []
then {choose LADRLIST, ERR0
with (⌊ERR0⌋ ∨ ERR0 = ESUCCESS) ∧ ¬ dups(PSTORE[PNL.last].ladrlist + LADRLIST) ∧ # LADRLIST ≤ # GNDLIST
∧ inv-flashsize(prefixn(# LADRLIST, GNDLIST), LADRLIST) ∧ (ERR0 = ESUCCESS ↔ # LADRLIST = # GNDLIST)
in {ADRLIST := LADRLIST.to-adr(PNL.last), ERR := ERR0;
PSTORE[PNL.last].gndlist := PSTORE[PNL.last].gndlist + prefixn(# LADRLIST, GNDLIST);
PSTORE[PNL.last].ladrlist := PSTORE[PNL.last].ladrlist + LADRLIST; if ERR ≠ ESUCCESS then ADRLIST := ?};
ISYNCED := ?}
else abort
}
sync:
index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISYNCED := true else ISYNCED := ?}
}
set-gblock-refsize:
index_set_gblock_refsize#(LNUM, N, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)
precondition LNUM ∈ PSTORE;
postcondition true;
{if LNUM ∈ PSTORE then PSTORE[LNUM].ref-size := N else abort
}
get-gblock-refsize:
index_get_gblock_refsize#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N)
precondition LNUM ∈ PSTORE;
postcondition true;
{if LNUM ∈ PSTORE then N := PSTORE[LNUM].ref-size else abort
}
get-block-free-size:
index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N)
precondition true;
postcondition true;
{choose N0 with N0 ≤ LEB_SIZE in N := N0
}
is-log-empty:
index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?)
precondition true;
postcondition true;
{EMPTY? := PNL = []
}
allocate-gnd:
index_allocate_gnd#(PRI, PFI, PSTORE0, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE, PNL; ERR)
precondition ISYNCED;
postcondition true;
{if ISYNCED
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then choose N with ¬ N ∈ PSTORE in PSTORE[N] := groupblock([], [], 0), PNL := PNL + N, PINVAL := PINVAL -- N}
else abort
}
deallocate-gnd:
index_deallocate_gnd#(N, PRI, PFI, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE; ERR)
precondition ISYNCED ∧ N ∈ PSTORE ∧ ¬ N ∈ PNL;
postcondition true;
{if ISYNCED ∧ N ∈ PSTORE ∧ ¬ N ∈ PNL
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PSTORE := PSTORE -- N, PINVAL := PINVAL ++ N}
else abort
}
commit:
index_commit#(PMAXINO0, PRI, ISYNCED; P_OS0, PINVAL, PSTORE, PFI, PSTORE0, PNL, PMAXINO, P_OS; ERR)
precondition ISYNCED ∧ dom remove-refsize0(PSTORE) ∩ PINVAL = ∅;
postcondition true;
{if ISYNCED ∧ dom remove-refsize0(PSTORE) ∩ PINVAL = ∅
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {PSTORE := remove-refsize0(PSTORE); PSTORE0 := PSTORE; PINVAL := ∅; P_OS := P_OS0; PNL := []; PMAXINO := PMAXINO0;
PFI := PRI};
P_OS0 := ?}
else abort
}
requires-commit:
index_requires_commit#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; COMMIT?)
precondition true;
postcondition true;
{COMMIT? := ?
}
format:
index_format#(VOLSIZE, SIZE, PMAXINO0; ; PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then PMAXINO := PMAXINO0, ISYNCED := true, P_OS := ∅, PNL := [], PSTORE := ∅, PSTORE0 := ∅, PINVAL := ∅, PRI := ∅, PFI := ∅
else PMAXINO := ?, ISYNCED := ?, P_OS := ?, PNL := ?, PSTORE := ?, PSTORE0 := ?, PINVAL := ?, PRI := ?, PFI := ?}
else abort
}
recovery:
index_recover#(; PMAXINO0, PNL0, P_OS0, PFI, PNL, PMAXINO, P_OS, PINVAL, PSTORE, PSTORE0; PRI, ISYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then PMAXINO0 := PMAXINO, ISYNCED := true, PNL0 := PNL, P_OS0 := P_OS, PRI := PFI
else PINVAL := ?, ISYNCED := ?, PSTORE := ?, PSTORE0 := ?, PNL := ?, PMAXINO := ?, P_OS := ?, PMAXINO0 := ?, PNL0 := ?, P_OS0 := ?,
PRI := ?, PFI := ?}
}
end data asm specification