[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
gjournal
using index-asm, gjournal-abs,
debug
procedures gjournal_index_newino# : key × nat nonfunctional ;
gjournal_index_contains#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : bool : error
nondeterministic;
gjournal_index_lookup#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : bool × node : error
nondeterministic;
gjournal_index_store#
key × address × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : nat × node-index × group-store
nonfunctional
nondeterministic;
gjournal_index_remove# key × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : node-index × group-store
nonfunctional
nondeterministic;
gjournal_index_truncate#
key × nat × bool × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : node-index × group-store
nonfunctional
nondeterministic;
gjournal_remove_addresses#
bool × node-index × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : address-set × group-store
nonfunctional
nondeterministic;
gjournal_index_entries#
key × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : stringset : error
nondeterministic;
gjournal_journal_get#
address × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : node : error
nondeterministic;
gjournal_journal_allocate#
nat × node-index × node-index × group-store × nat × nat-set : bool × nat-set × group-store × nat-list × bool : error
nondeterministic;
gjournal_journal_transaction# node-list × nat : : group-node-list × nat ;
gjournal_journal_addn#
node-list × bool × node-index × node-index × group-store × nat × nat-set
: address-list × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_add1#
node × bool × node-index × node-index × group-store × nat × nat-set
: address × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_add2#
node × node × bool × node-index × node-index × group-store × nat × nat-set
: address × address × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_add3#
node × node × node × bool × node-index × node-index × group-store × nat × nat-set
: address × address × address × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_add4#
node × node × node × node × bool × node-index × node-index × group-store × nat × nat-set
: address × address × address × address × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_add5#
node × node × node × node × node × bool × node-index × node-index × group-store × nat × nat-set
: address × address × address × address × address × bool × nat × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_journal_sync# node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set : bool : error
nondeterministic;
gjournal_journal_gc#
bool × node-index × group-store × nat × nat-set : bool × nat × nat × node-index × nat-set × group-store × nat-list × bool
nonfunctional
nondeterministic;
gjournal_gc_referenced_nodes#
nat × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool
: address-list × group-node-list
: node-list × error
nondeterministic;
gjournal_gc_copy#
bool × node-index × group-store × nat × nat-set
: node-list × bool × nat × nat × node-index × nat-set × group-store × nat-list × bool
: error
nondeterministic;
gjournal_split_nodes# nat : node-list × node-list nonfunctional ;
gjournal_gc_update_index#
bool × node-index × nat-set × group-store × nat-list × nat × nat-set × bool : address-list × node-list × nat × node-index × group-store
nonfunctional
nondeterministic;
gjournal_recover#
bool
: address-list × key-set × nat × nat-set × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set ×
bool
: bool × nat × bool × error
nondeterministic;
gjournal_restore_log#
nat-list × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : address-list : error
nondeterministic;
gjournal_remove_nonend_blocks#
nat × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : address-list : error
nondeterministic;
gjournal_check_commit#
nat × nat-set × node-index : node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : error
nondeterministic;
gjournal_commit#
nat × nat-set × node-index : node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool : error
nondeterministic;
gjournal_format#
nat × nat × bool
: nat × node-index × node-index × nat-set × group-store × group-store × nat-list × nat × nat-set × bool
: bool × nat × nat-set × bool × error
nondeterministic;
gjournal_orphans_contains# key × nat-set : bool nonfunctional ;
gjournal_orphans_insert# key : nat × nat-set nonfunctional ;
gjournal_orphans_remove# key : nat-set nonfunctional ;
variables KEY : key flexible;
AS : address-set flexible;
NAMES : stringset flexible;
EXISTS : bool flexible;
KS : key-set flexible;
OLDADR : address flexible;
DONE : bool flexible;
FIRST? : bool flexible;
LAST? : bool flexible;
SQNUM : nat flexible;
SIZE0 : nat flexible;
SIZE1 : nat flexible;
SIZE2 : nat flexible;
SIZE3 : nat flexible;
SIZE4 : nat flexible;
ADR : address flexible;
ADR0 : address flexible;
ADR1 : address flexible;
ADR2 : address flexible;
ADR3 : address flexible;
ADR4 : address flexible;
ADR5 : address flexible;
ND : node flexible;
ND0 : node flexible;
ND1 : node flexible;
ND2 : node flexible;
ND3 : node flexible;
ND4 : node flexible;
ND5 : node flexible;
NDLIST : node-list flexible;
NDLIST0 : node-list flexible;
GND : group-node flexible;
GND0 : group-node flexible;
GND1 : group-node flexible;
GND2 : group-node flexible;
GND3 : group-node flexible;
GND4 : group-node flexible;
LOG : address-list flexible;
ADRLIST0 : address-list flexible;
ADRLIST1 : address-list flexible;
KEYLIST : key-list flexible;
GNDLIST1 : group-node-list flexible;
JMAXINO : nat flexible;
JRO : nat-set flexible;
JRO0 : nat-set flexible;
JGINVAL : nat-set flexible;
JNL : nat-list flexible;
JVALID : bool flexible;
DOSYNC : bool flexible;
DOSYNC0 : bool flexible;
jro : nat-set;
p_os : nat-set;
jmaxino : nat;
pmaxino : nat;
jvalid : bool;
state variables JVALID : bool flexible;
SQNUM : nat flexible;
JMAXINO : nat flexible;
JRO : nat-set flexible;
DOSYNC : bool flexible;
initialization procedure gjournal_format#
if ERR = ESUCCESS
sequential
invariants maxino
: ⊦ JRO < JMAXINO ∧ P_OS < PMAXINO ∧ PMAXINO ≤ JMAXINO ∧ PRI.inos < JMAXINO ∧ PFI.inos < PMAXINO ∧ JMAXINO ≠ 0 ∧ PMAXINO ≠ 0;
journal-head : ⊦ JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL);
lebs-index : ⊦ PRI.lebs ⊆ dom PSTORE ∧ PFI.lebs ⊆ dom PSTORE0;
refsize-cons : ⊦ refsize-cons(PSTORE, range PRI) ∧ refsize-cons(PSTORE0, range PFI);
recovery procedure gjournal_recover#
if ERR = ESUCCESS
declarations newino:
gjournal_index_newino#(; KEY, JMAXINO)
precondition true;
postcondition true;
{{KEY := inodekey(JMAXINO); JMAXINO := JMAXINO + 1}
}
contains:
gjournal_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR)
precondition true;
postcondition true;
{index_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR)
}
lookup:
gjournal_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ND; ERR)
precondition ri-cons(PRI, nodes(PSTORE ↓, PINVAL));
postcondition true;
{if ri-cons(PRI, nodes(PSTORE ↓, PINVAL))
then let ADR = ?
in {index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR; ERR);
if ERR = ESUCCESS ∧ EXISTS
then let GND = ?
in {index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR);
if ERR = ESUCCESS then ND := GND.nd}}
else abort
}
store:
gjournal_index_store#(KEY, ADR, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JMAXINO, PRI, PSTORE)
precondition ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd);
postcondition PSTORE =○refsize PSTORE` ∧ PRI = (PRI`)[KEY, ADR];
{if ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd)
then let EXISTS = ?, OLDADR = ?
in {index_index_store#(KEY, ADR, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI);
let N = ?
in {if EXISTS
then {index_get_gblock_refsize#(OLDADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
index_set_gblock_refsize#
(OLDADR.lnum, N - OLDADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)};
index_get_gblock_refsize#(ADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
index_set_gblock_refsize#(ADR.lnum, N + ADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)};
JMAXINO := max(KEY.ino + 1, JMAXINO)}
else abort
}
remove:
gjournal_index_remove#(KEY, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PRI, PSTORE)
precondition true;
postcondition true;
{let EXISTS = ?, OLDADR = ?
in {index_index_remove#(KEY, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI);
if EXISTS
then let N = ?
in {index_get_gblock_refsize#(OLDADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
index_set_gblock_refsize#
(OLDADR.lnum, N - OLDADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)}}
}
truncate:
gjournal_index_truncate#(KEY, N, JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PRI, PSTORE)
precondition true;
postcondition PSTORE =○refsize PSTORE`;
{let AS = ?
in {index_index_truncate#(KEY, N, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PRI);
gjournal_remove_addresses#(JVALID, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PSTORE)}
}
remove-addresses
: gjournal_remove_addresses#(JVALID, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PSTORE)
{while AS ≠ ∅
do {/* (inv-truncate
: invariant (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) ∧ dom PSTORE = dom PSTORE` ∧ AS ∩ range PRI = ∅
∧ AS.lebs ⊆ dom PSTORE ∧ refsize-cons(PSTORE, range PRI ∪ AS) ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL)
∧ PSTORE =○refsize PSTORE`
wfbound # AS)
*/;
choose N, ADR
with ADR ∈ AS
in {index_get_gblock_refsize#(ADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
index_set_gblock_refsize#(ADR.lnum, N - ADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE);
AS := AS -- ADR}}
}
;
entries:
gjournal_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR)
precondition true;
postcondition true;
{index_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR)
}
get:
gjournal_journal_get#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ND; ERR)
precondition ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL;
postcondition true;
{if ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL
then choose GND
with true
in {index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR);
if ERR = ESUCCESS then ND := GND.nd}
else abort
}
allocate:
gjournal_journal_allocate#(SIZE, PRI, PFI, PSTORE0, PMAXINO, P_OS; JVALID, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ dom PSTORE` ⊆ dom PSTORE ∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅
∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) ∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)
∧ (ERR = ESUCCESS → JVALID ∧ PNL ≠ [])
;
{let N = ?
in {index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
if SIZE > N
then ERR := ENOSPC
else let N = ?, EMPTY? = ?
in {index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?);
if ¬ EMPTY? ∧ JVALID
then index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
if ¬ EMPTY? ∧ JVALID ∧ SIZE ≤ N
then ERR := ESUCCESS
else {index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR);
if ERR = ESUCCESS
then index_allocate_gnd#(PRI, PFI, PSTORE0, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE, PNL; ERR);
if ERR = ESUCCESS then JVALID := true}}}
}
transaction:
gjournal_journal_transaction#(NDLIST, SQNUM; ; GNDLIST, SIZE)
precondition true;
postcondition transaction(NDLIST, GNDLIST) ∧ SIZE = GNDLIST.flashsize;
{{SIZE := 0; GNDLIST := [];
let FIRST? = true
in while NDLIST ≠ []
do {/* (inv-transaction
: invariant ∃ ndx.
NDLIST` = ndx + NDLIST ∧ (NDLIST = [] → transaction(NDLIST`, GNDLIST))
∧ (NDLIST ≠ [] → transaction-prefix(NDLIST`, GNDLIST) ∧ # GNDLIST = # ndx)
∧ SIZE = GNDLIST.flashsize ∧ (FIRST? ↔ ndx = [])
wfbound # NDLIST)
*/;
let LAST? = # NDLIST = 1
in let GND = mkgnode(NDLIST.head, SQNUM + # GNDLIST, FIRST?, LAST?)
in {GNDLIST := GNDLIST + GND; SIZE := SIZE + GND.flashsize; NDLIST := NDLIST.tail; FIRST? := false}}}
}
addn:
gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ dom PSTORE` ⊆ dom PSTORE ∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅
∧ ( ERR = ESUCCESS
→ # ADRLIST = # NDLIST ∧ ¬ dups(ADRLIST) ∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL)
∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) + ADRLIST
∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)[ADRLIST, NDLIST] ∧ new(ADRLIST, nodes(PSTORE` ↓, PINVAL`)))
∧ ( ERR ≠ ESUCCESS
→ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) ∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`))
;
{let GNDLIST = ?, SIZE = ?
in {gjournal_journal_transaction#(NDLIST, SQNUM; ; GNDLIST, SIZE);
gjournal_journal_allocate#(SIZE, PRI, PFI, PSTORE0, PMAXINO, P_OS; JVALID, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then index_add_gnds#(GNDLIST, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS; ADRLIST, PSTORE; ISYNCED, ERR);
if ERR = ESUCCESS
then {SQNUM := SQNUM + # NDLIST;
if DOSYNC then let ERR0 = ? in index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR0)}
else JVALID := false}
}
add1:
gjournal_journal_add1#(ND1, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition true;
postcondition true;
{let NDLIST = ND1 ', ADRLIST = ?
in {gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then ADR1 := ADRLIST[0]}
}
add2:
gjournal_journal_add2#
(ND1, ND2, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition true;
postcondition true;
{let NDLIST = ND1 + ND2 ', ADRLIST = ?
in {gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]}}
}
add3:
gjournal_journal_add3#
(ND1, ND2, ND3, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, ADR3, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition true;
postcondition true;
{let NDLIST = ND1 + ND2 + ND3 ', ADRLIST = ?
in {gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]}}
}
add4:
gjournal_journal_add4#
(ND1, ND2, ND3, ND4, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS
; ADR1, ADR2, ADR3, ADR4, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED
; ERR
)
precondition true;
postcondition true;
{let NDLIST = ND1 + ND2 + ND3 + ND4 ', ADRLIST = ?
in {gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]; ADR4 := ADRLIST[3]}}
}
add5:
gjournal_journal_add5#
(ND1, ND2, ND3, ND4, ND5, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS
; ADR1, ADR2, ADR3, ADR4, ADR5, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED
; ERR
)
precondition true;
postcondition true;
{let NDLIST = ND1 + ND2 + ND3 + ND4 + ND5 ', ADRLIST = ?
in {gjournal_journal_addn#
(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]; ADR4 := ADRLIST[3]; ADR5 := ADRLIST[4]}}
}
sync:
gjournal_journal_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ISYNCED; ERR)
precondition true;
postcondition true;
{index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR)
}
gc:
gjournal_journal_gc#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED)
precondition ri-cons(PRI, nodes(PSTORE ↓, PINVAL));
postcondition true;
{if ri-cons(PRI, nodes(PSTORE ↓, PINVAL))
then let LNUM = ?, ERR = ?
in {index_get_gc_block#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LNUM; ERR);
if ERR = ESUCCESS
then let N = ?
in {debug#("gjournal: garbage collecting LEB " + LNUM.toString);
index_get_gblock_refsize#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
if N ≠ 0
then let ADRLIST = [], GNDLIST = [], NDLIST = []
in {index_read_gblock_nodes#
(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; ERR);
if ERR ≠ ESUCCESS
then debug#("gjournal: failed to read LEB " + LNUM.toString + " during GC")
else gjournal_gc_referenced_nodes#
(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; NDLIST, ERR);
if ERR = ESUCCESS
then {gjournal_gc_copy#
(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS
; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED
; ERR);
if ERR ≠ ESUCCESS
then debug#
("gjournal: failed to copy nodes of LEB " + LNUM.toString + " to journal head during GC")}}};
if ERR = ESUCCESS then index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR);
if ERR = ESUCCESS then index_deallocate_gnd#(LNUM, PRI, PFI, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE; ERR)}
else abort
}
gc-referenced-nodes
: gjournal_gc_referenced_nodes#
(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; NDLIST, ERR)
{ERR := ESUCCESS; NDLIST := [];
while ERR = ESUCCESS ∧ ADRLIST ≠ []
do {/* (prepost-gc-referenced-nodes
: invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ (∃ ax0, gndx0.
ADRLIST` = ax0 + ADRLIST ∧ GNDLIST` = gndx0 + GNDLIST ∧ # ADRLIST` = # GNDLIST`
∧ # ADRLIST = # GNDLIST ∧ NDLIST = nodes(PSTORE ↓, PINVAL)[referenced-adrs(ax0, PRI)]))
wfbound (ERR = ESUCCESS ⊃ # ADRLIST;0))
*/;
let EXISTS = ?, ADR0 = ?
in {let ADR = ADRLIST.head, GND = GNDLIST.head
in let KEY = GND.nd.key
in {index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR0; ERR);
if ERR = ESUCCESS ∧ EXISTS ∧ ADR0 = ADR then NDLIST := NDLIST + GND.nd};
if ERR = ESUCCESS then {ADRLIST := ADRLIST.tail; GNDLIST := GNDLIST.tail}}}
}
;
gc-copy:
gjournal_gc_copy#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED; ERR)
precondition NDLIST.keys.toSet ⊆ dom PRI ∧ ¬ dups(NDLIST.keys) ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ key-cons(NDLIST);
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ JMAXINO` ≤ JMAXINO ∧ dom PSTORE` ⊆ dom PSTORE
∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅
∧ (∃ ax, ndx0, ndx1.
NDLIST` = ndx0 + ndx1 ∧ (ERR = ESUCCESS → ndx1 = []) ∧ new(ax, nodes(PSTORE` ↓, PINVAL`))
∧ # ax = # ndx0 ∧ ¬ dups(ax) ∧ PRI = (PRI`)[ndx0.keys, ax]
∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)[ax, ndx0]
∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) + ax)
;
{if NDLIST.keys.toSet ⊆ dom PRI ∧ ¬ dups(NDLIST.keys) ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ key-cons(NDLIST)
then {ERR := ESUCCESS;
while ERR = ESUCCESS ∧ NDLIST ≠ []
do {/* (inv-gc-copy
: invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (∃ ndx0. NDLIST` = ndx0 + NDLIST) ∧ JMAXINO ≥ JMAXINO`
∧ (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) ∧ PRI.inos < JMAXINO
∧ PRI.lebs ⊆ dom PSTORE ∧ refsize-cons(PSTORE, range PRI) ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL)
∧ ri-inj(PRI) ∧ NDLIST.keys.toSet ⊆ dom PRI ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL)
∧ dom PSTORE` ⊆ dom PSTORE ∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅
∧ (∃ ax, ndx0, ndx1.
NDLIST` = ndx0 + ndx1 ∧ (ERR = ESUCCESS → ndx1 = NDLIST) ∧ new(ax, nodes(PSTORE` ↓, PINVAL`))
∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ PRI = (PRI`)[ndx0.keys, ax]
∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)[ax, ndx0]
∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) + ax)
wfbound (ERR = ESUCCESS ⊃ # NDLIST;0))
*/;
let SIZE = 0, EMPTY? = ?
in {index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?);
if ¬ EMPTY?
then {index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; SIZE);
if SIZE < NDLIST.head.flashsize then SIZE := 0};
let NDLIST0 = [], ADRLIST = [], N = ?
in {index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N);
gjournal_split_nodes#(N - SIZE; NDLIST, NDLIST0);
if NDLIST0 = []
then ERR := EINVAL
else {gjournal_journal_addn#
(NDLIST0, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR);
if ERR = ESUCCESS
then gjournal_gc_update_index#
(JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, NDLIST0, JMAXINO, PRI, PSTORE)}}}}}
else abort
}
split-nodes
: gjournal_split_nodes#(SIZE; NDLIST, NDLIST0)
{NDLIST0 := [];
while NDLIST ≠ [] ∧ NDLIST.head.flashsize ≤ SIZE
do {/* (prepost-split-nodes: invariant NDLIST` = NDLIST0 + NDLIST ∧ SIZE` = NDLIST0.flashsize + SIZE wfbound # NDLIST) */;
let ND = NDLIST.head in {NDLIST0 := NDLIST0 + ND; NDLIST := NDLIST.tail; SIZE := SIZE - ND.flashsize}}
}
;
gc-update-index:
gjournal_gc_update_index#(JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, NDLIST, JMAXINO, PRI, PSTORE)
precondition NDLIST.keys.toSet ⊆ dom PRI ∧ # ADRLIST = # NDLIST ∧ key-cons(NDLIST) ∧ ADRLIST.toSet ∩ range PRI = ∅
∧ ¬ dups(ADRLIST) ∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL)
;
postcondition PRI = (PRI`)[NDLIST`.keys, ADRLIST`] ∧ dom PSTORE = dom PSTORE`
∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`) ∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓)
∧ JMAXINO` ≤ JMAXINO
;
{if NDLIST.keys.toSet ⊆ dom PRI ∧ # ADRLIST = # NDLIST ∧ key-cons(NDLIST) ∧ ADRLIST.toSet ∩ range PRI = ∅ ∧ ¬ dups(ADRLIST)
∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL)
then while ADRLIST ≠ []
do {/* (inv-gc-update-index
: invariant # ADRLIST` = # NDLIST`
∧ (∃ ax0, ndx0.
# ax0 = # ndx0 ∧ ADRLIST` = ax0 + ADRLIST ∧ NDLIST` = ndx0 + NDLIST
∧ PRI = (PRI`)[ndx0.keys, ax0])
∧ dom PRI = dom PRI` ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL) ∧ JMAXINO` ≤ JMAXINO
∧ PRI.inos < JMAXINO ∧ refsize-cons(PSTORE, range PRI) ∧ ri-inj(PRI) ∧ PRI.lebs ⊆ dom PSTORE
∧ dom PSTORE = dom PSTORE` ∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL)
∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`) ∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓)
∧ (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL))
wfbound # ADRLIST)
*/;
gjournal_index_store#
(NDLIST.head.key, ADRLIST.head, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JMAXINO, PRI, PSTORE);
ADRLIST := ADRLIST.tail; NDLIST := NDLIST.tail}
else abort
}
recover:
gjournal_recover#
(DOSYNC0; LOG, KS, JMAXINO, JRO, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JVALID, SQNUM, DOSYNC, ERR)
precondition true;
postcondition true;
{{SQNUM := 0; JVALID := false; DOSYNC := DOSYNC0;
let JNL = ?
in {index_recover#(; JMAXINO, JNL, JRO, PFI, PNL, PMAXINO, P_OS, PINVAL, PSTORE, PSTORE0; PRI, ISYNCED, ERR);
if ERR ≠ ESUCCESS
then debug#("gjournal: persistence recover failed")
else {gjournal_restore_log#(JNL, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR); KS := JRO.keys}}}
}
restore-log
: gjournal_restore_log#(JNL, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR)
{LOG := []; ERR := ESUCCESS;
while JNL ≠ [] ∧ ERR = ESUCCESS
do {/* (term-restore-log: invariant elems JNL ⊆ dom PSTORE ∧ elems JNL ∩ PINVAL = ∅ ∧ inv(PSTORE) wfbound # JNL) */;
gjournal_remove_nonend_blocks#(JNL.head, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR);
JNL := JNL.tail}
}
;
remove-nonend-blocks
: gjournal_remove_nonend_blocks#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR)
{let GNDLIST = [], DONE = false
in {index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG, GNDLIST; ERR);
if ERR = ESUCCESS
then while ¬ DONE ∧ GNDLIST ≠ []
do {/* (term-remove-nonend-blocks: invariant # GNDLIST ≤ # LOG ∧ inv(PSTORE) wfbound (DONE ⊃ 0;# GNDLIST)) */;
if GNDLIST.last.end then DONE := true else {LOG := LOG.butlast; GNDLIST := GNDLIST.butlast}}}
}
;
check-commit:
gjournal_check_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR)
precondition dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE);
postcondition true;
{if dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE)
then let COMMIT? = false
in {index_requires_commit#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; COMMIT?);
if COMMIT?
then gjournal_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR)
else ERR := ESUCCESS}
else abort
}
commit:
gjournal_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR)
precondition dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE);
postcondition true;
{if dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE)
then {index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR);
if ERR = ESUCCESS
then let JRO0 = JRO in index_commit#(JMAXINO, PRI, ISYNCED; JRO0, PINVAL, PSTORE, PFI, PSTORE0, PNL, PMAXINO, P_OS; ERR)}
else abort
}
format:
gjournal_format#
(VOLSIZE, SIZE, DOSYNC0; JMAXINO, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JVALID, SQNUM, JRO, DOSYNC, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {JMAXINO := ROOT_INO + 1; SQNUM := 0; JVALID := true; DOSYNC := DOSYNC0;
index_format#(VOLSIZE, SIZE, JMAXINO; ; PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED, ERR);
if ERR ≠ ESUCCESS then debug#("gjournal: persistence format failed"); JRO := ∅}
else abort
}
orphans-contains:
gjournal_orphans_contains#(KEY, JRO; EXISTS)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then EXISTS := KEY.ino ∈ JRO else abort
}
orphans-insert:
gjournal_orphans_insert#(KEY; JMAXINO, JRO)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then {JRO := JRO ++ KEY.ino; JMAXINO := max(KEY.ino + 1, JMAXINO)} else abort
}
orphans-remove:
gjournal_orphans_remove#(KEY; JRO)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then JRO := JRO -- KEY.ino else abort
}
end data asm specification