[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
persistence
using awbuf-asm
,
persistence-base
procedures persistence_add_gnds#
group-node-list × nat-list × nat × address × nat × nat-list × lp-array × nat-set × bufleb
: address-list × lp-array × avolume × bool
: error
nondeterministic;
persistence_encode_group_nodes# group-node-list × nat × nat : : buffer × address-list × error nondeterministic;
persistence_add_ind#
index-node × nat × address × nat × nat-list × lp-array × nat-set × bufleb : address × lp-array × avolume × bool : error
nondeterministic;
persistence_read_gnd# address × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : group-node : error
nondeterministic;
persistence_read_ind# address × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : index-node : error
nondeterministic;
persistence_read_gblock_nodes#
nat × nat × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : address-list × group-node-list : error
nondeterministic;
persistence_get_leb_size# nat : : nat ;
persistence_set_iblock_refsize# nat × nat : lp-array nonfunctional ;
persistence_get_iblock_refsize# nat × lp-array : : nat ;
persistence_set_gblock_refsize# nat × nat × nat-list : lp-array × binheap nonfunctional ;
persistence_get_gblock_refsize# nat × lp-array : : nat ;
persistence_get_block_free_size# lp-array × nat × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : nat
nondeterministic;
persistence_get_gc_block# binheap : nat : error nondeterministic;
persistence_allocate_leb#
address × nat × nat-list × lp-array × nat-set × bufleb × bool : nat × lp-array × nat-list × avolume : error
nondeterministic;
persistence_allocate_gnd#
address × nat × lp-array × nat-set × bool : nat-list × lp-array × nat-list × nat-list × avolume × bufleb : error
nondeterministic;
persistence_is_log_empty# nat-list : : bool ;
persistence_allocate_ind# address × nat × nat-list × lp-array × nat-set × bool : lp-array × nat-list × avolume × bufleb : error
nondeterministic;
persistence_deallocate_gnd#
nat × nat-list × address × nat × nat-list × lp-array × nat-set × bufleb × bool : lp-array × nat-list × binheap × avolume : error
nondeterministic;
persistence_sync# nat × address × nat × nat-list × lp-array × nat-set × bufleb : lp-array × avolume × bool : error
nondeterministic;
persistence_encode_padding_node# : buffer : error nondeterministic;
persistence_cleanup_lpt# address × nat × nat-list × lp-array × nat-set × bufleb × bool : lp-array × nat-list × binheap × avolume
nonfunctional
;
persistence_gc_heap_add_log# : nat-list × lp-array × binheap nonfunctional ;
persistence_commit#
address × nat
: nat-set × nat-list × lp-array × nat-list × binheap × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool
: error
nondeterministic;
persistence_requires_commit# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : bool nondeterministic;
persistence_is_readonly# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : bool ;
persistence_format#
nat × nat × nat
: lp-array × nat-list × binheap × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool × nat-list × nat
: error
nondeterministic;
persistence_create_freelist# lp-array : nat-list nonfunctional ;
persistence_recover#
: address × nat × nat-list × nat-set × nat-list × lp-array × nat-list × binheap × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
: error
nondeterministic;
persistence_replay_log# nat : nat-list × lp-array nonfunctional ;
persistence_replay_lpt# nat-list × nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool : lp-array × avolume
nonfunctional
;
persistence_create_gcheap# nat-list : lp-array × binheap nonfunctional ;
variables LOG : nat-list flexible;
LOG0 : nat-list flexible;
FREELIST : nat-list flexible;
SIZE : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
N : nat flexible;
FLASHSIZE : nat flexible;
PAGESIZE : nat flexible;
LEBSIZE : nat flexible;
ORPHANS : nat-set flexible;
ORPHANS0 : nat-set flexible;
LPT : lp-array flexible;
LPT0 : lp-array flexible;
GCHEAP : binheap flexible;
ADR : address flexible;
IND : index-node flexible;
ADRLIST : address-list flexible;
NODELIST : group-node-list flexible;
KI : keyindex flexible;
ROFS : bool flexible;
log : nat-list;
EMPTY? : bool flexible;
IDX : nat flexible;
state variables LOG : nat-list flexible;
LPT : lp-array flexible;
FREELIST : nat-list flexible;
GCHEAP : binheap flexible;
LEBSIZE : nat flexible;
initialization procedure persistence_format#
if ERR = ESUCCESS
sequential
invariants free-unref : ⊦ lpt-free-unref(LPT) ∧ lpt-free-unref(WLPT);
freelist : ⊦ freelist-cons(LPT, FREELIST);
ram-flash-log : ⊦ LOG = WLOG;
bin-heap : ⊦ bin-heap-inv(GCHEAP, LPT) ∧ keyset(GCHEAP) = gc-heap(LPT, LOG);
wbufs : ⊦ bufs-log-only(WBUFLEB, LOG, LPT);
ram-lpt-size : ⊦ # LPT = # WVOL;
log : ⊦ ¬ dups(LOG) ∧ log-group-block(LOG, LPT);
buffered-ro-rw-mode : ⊦ buf-ro-rw-mode(AROFS, WBUFLEB, LPT, WVOL);
lpt-leb-size : ⊦ lpt-leb-size(LPT) ∧ lpt-leb-size(WLPT);
lpt-ram-flash : ⊦ lpt-ram-flash(LPT, WLPT, LOG);
lebsize : ⊦ LEBSIZE = LEB_SIZE;
recovery procedure persistence_recover#
if ERR = ESUCCESS
declarations add-gnds:
persistence_add_gnds#(NODELIST, LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; ADRLIST, LPT, WVOL, AROFS; ERR)
precondition ¬ AROFS
→ WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_GROUP_NODES ∧ WBUFLEB.leb ∈ LOG
∧ WVOL[WBUFLEB.leb].mapped?
∧ ( NODELIST ≠ [] ∧ LPT[WBUFLEB.leb].size + NODELIST.flashsize ≤ LEB_SIZE
→ LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data)
;
postcondition true;
{if ¬ AROFS
→ WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_GROUP_NODES ∧ WBUFLEB.leb ∈ LOG
∧ WVOL[WBUFLEB.leb].mapped?
∧ (NODELIST ≠ [] ∧ LPT[WBUFLEB.leb].size + NODELIST.flashsize ≤ LEB_SIZE → LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data)
then let AROFS0 = ?
in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0);
if AROFS0
then ERR := EROFS
else if NODELIST = []
then {ADRLIST := []; ERR := ESUCCESS}
else let BUF = ?, WBUFLEB0 = ?
in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0);
persistence_encode_group_nodes#(NODELIST, WBUFLEB0.leb, LPT[WBUFLEB0.leb].size; ; BUF, ADRLIST, ERR);
if ERR = ESUCCESS
then if ¬ LPT[WBUFLEB0.leb].size + # BUF ≤ LEBSIZE
then {debug#("persistence: trying to write beyond LEB size");
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS);
ERR := ENOSPC}
else {awbuf_write_buf#
(# BUF, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR);
if ERR = ESUCCESS
then LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + # BUF
else {debug#("persistence: adding group node to LEB " + WBUFLEB0.leb.toString + " failed");
LPT[WBUFLEB0.leb].size := LEBSIZE}}
else {debug#("persistence: could not encode group node");
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}}
else abort
}
encode-group-nodes
: persistence_encode_group_nodes#(NODELIST, LNUM, N; ; BUF, ADRLIST, ERR)
{ERR := ESUCCESS; BUF := mkbuf(NODELIST.flashsize); ADRLIST := [];
let IDX = 0, OFFSET = 0
in while ERR = ESUCCESS ∧ IDX < # NODELIST
do {/* (prepost-encode-group-nodes
: invariant IDX ≤ # NODELIST ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ # BUF = # BUF`
∧ (∃ gndx0, gndx1.
NODELIST = gndx0 + gndx1 ∧ # gndx0 = IDX ∧ OFFSET = gndx0.flashsize
∧ (∃ lax, buf0, buf1.
lax.to-adr(LNUM) = ADRLIST ∧ BUF = buf0 + buf1 ∧ # buf0 = OFFSET
∧ abs-nodes(buf0, N, gndx0, lax, false))))
wfbound # NODELIST - IDX)
*/;
let SIZE = ?
in {encode_group_node#(NODELIST[IDX], OFFSET; SIZE, BUF; ERR); ADRLIST := ADRLIST + @(LNUM, N + OFFSET, SIZE);
OFFSET := OFFSET + SIZE};
IDX := IDX + 1}
}
;
add-ind:
persistence_add_ind#(IND, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; ADR, LPT, WVOL, AROFS; ERR)
precondition ¬ AROFS
→ WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_INDEX_NODES ∧ WVOL[WBUFLEB.leb].mapped?
∧ (LPT[WBUFLEB.leb].size + IND.flashsize ≤ LEB_SIZE → LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data)
;
postcondition true;
{if ¬ AROFS
→ WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_INDEX_NODES ∧ WVOL[WBUFLEB.leb].mapped?
∧ (LPT[WBUFLEB.leb].size + IND.flashsize ≤ LEB_SIZE → LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data)
then let AROFS0 = ?
in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0);
if AROFS0
then ERR := EROFS
else let BUF = mkbuf(IND.flashsize), SIZE = ?, WBUFLEB0 = ?
in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0);
encode_index_node#(IND, 0; SIZE, BUF; ERR);
if ERR = ESUCCESS
then if ¬ LPT[WBUFLEB0.leb].size + SIZE ≤ LEBSIZE
then {debug#("persistence: trying to write beyond LEB size");
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS);
ERR := ENOSPC}
else {awbuf_write_buf#(SIZE, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR);
if ERR = ESUCCESS
then {ADR := @(WBUFLEB0.leb, LPT[WBUFLEB0.leb].size, SIZE);
LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + SIZE}
else LPT[WBUFLEB0.leb].size := LEBSIZE}
else {debug#("persistence: could not encode index node");
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}}
else abort
}
read-gnd:
persistence_read_gnd#(ADR, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; GND; ERR)
precondition ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data
∧ (∃ gnd. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), gnd))
;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), GND));
{if ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data
∧ (∃ gnd. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), gnd))
then let BUF = mkbuf(ADR.size)
in {awbuf_read_buf#(ADR.lnum, ADR.pos, ADR.size, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR);
if ERR = ESUCCESS then decode_group_node#(0, ADR.size, BUF; GND; ERR)}
else abort
}
read-ind:
persistence_read_ind#(ADR, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; IND; ERR)
precondition ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data
∧ (∃ ind. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), ind))
;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), IND));
{if ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data
∧ (∃ ind. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), ind))
then let BUF = mkbuf(ADR.size)
in {awbuf_read_buf#(ADR.lnum, ADR.pos, ADR.size, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR);
if ERR = ESUCCESS then decode_index_node#(0, ADR.size, BUF; IND; ERR)}
else abort
}
read-gblock-nodes:
persistence_read_gblock_nodes#
(LNUM, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ADRLIST, NODELIST; ERR)
precondition LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ (∃ gndx, lax. abs-nodes(WVOL[LNUM].data, gndx, lax, true));
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ (∃ lax, gndx.
ADRLIST = ADRLIST` + lax.to-adr(LNUM) ∧ NODELIST = NODELIST` + gndx
∧ abs-nodes(WVOL[LNUM].data, gndx, lax, true)))
;
{if LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ (∃ gndx, lax. abs-nodes(WVOL[LNUM].data, gndx, lax, true))
then let BUF = mkbuf(LEBSIZE), OFFSET = 0
in {awbuf_read_buf#(LNUM, 0, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR);
while ERR = ESUCCESS ∧ OFFSET < LEBSIZE
do {/* (inv-read-gblock-nodes
: invariant (ERR = ESUCCESS ∨ ERR = ENOENT ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS ∨ ERR = ENOENT
→ read-gblock-inv
(LNUM, OFFSET, ADRLIST, NODELIST, ADRLIST`, NODELIST`, WVOL[LNUM].data, ERR = ENOENT))
wfbound (ERR ≠ ESUCCESS ⊃ 0;LEBSIZE - OFFSET))
*/;
if ¬ OFFSET + NODE_HEADER_SIZE ≤ # BUF ∨ isempty(BUF, OFFSET, NODE_HEADER_SIZE)
then ERR := ENOENT
else let NDHD = ?
in {decode_header#(OFFSET, BUF; NDHD; ERR);
if ERR ≠ ESUCCESS
then debug#
( "persistence: read_gblock_nodes could not decode header in LEB " + LNUM.toString + " at offset "
+ OFFSET.toString)
else let SIZE = 2 * NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE)
in {if OFFSET + SIZE > LEBSIZE
then {debug#
( "persistence: read_gblock_nodes ignoring node of size " + SIZE.toString + " at offset "
+ OFFSET.toString + " in LEB " + LNUM.toString);
ERR := ENOENT}
else if ¬
range=
(BUF, OFFSET + NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE), validtrailer, 0,
NODE_HEADER_SIZE)
then {ERR := ENOENT;
debug#
( "persistence: read_gblock_nodes partial node at offset " + OFFSET.toString + " in LEB "
+ LNUM.toString)}
else if ¬ NDHD.ispadding
then let GND = ?
in {decode_group_node#(OFFSET, SIZE, BUF; GND; ERR);
if ERR ≠ ESUCCESS
then debug#
( "persistence: read_gblock_nodes could not decode node at offset "
+ OFFSET.toString + " in LEB " + LNUM.toString)
else {NODELIST := NODELIST + GND; ADRLIST := ADRLIST + @(LNUM, OFFSET, SIZE)}};
if ERR = ESUCCESS then OFFSET := OFFSET + SIZE}}};
if ERR = ENOENT then ERR := ESUCCESS}
else abort
}
get-leb-size:persistence_get_leb_size#(LEBSIZE; ; N) precondition true; postcondition true;{N := LEBSIZE}
set-iblock-refsize:
persistence_set_iblock_refsize#(LNUM, N; LPT)
precondition LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES;
postcondition true;
{if LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES then LPT[LNUM].ref-size := N else abort
}
get-iblock-refsize:
persistence_get_iblock_refsize#(LNUM, LPT; ; N)
precondition LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES;
postcondition true;
{if LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES then N := LPT[LNUM].ref-size else abort
}
set-gblock-refsize:
persistence_set_gblock_refsize#(LNUM, N, LOG; LPT, GCHEAP)
precondition LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES;
postcondition true;
{if LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES
then {LPT[LNUM].ref-size := N; if ¬ LNUM ∈ LOG then gc_heap_update#(LPT[LNUM].gcheapidx, N; GCHEAP, LPT)}
else abort
}
get-gblock-refsize:
persistence_get_gblock_refsize#(LNUM, LPT; ; N)
precondition LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES;
postcondition true;
{if LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES then N := LPT[LNUM].ref-size else abort
}
get-block-free-size:
persistence_get_block_free_size#(LPT, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N)
precondition true;
postcondition true;
{let WBUFLEB0 = ?
in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0);
if WBUFLEB0 = nobuffer then N := 0 else N := LEBSIZE - LPT[WBUFLEB0.leb].size}
}
get-gc-block:
persistence_get_gc_block#(GCHEAP; N; ERR)
precondition true;
postcondition (ERR = ENOSPC ∨ ERR = ESUCCESS) ∧ (ERR ≠ ESUCCESS → N = N`)
∧ (ERR = ESUCCESS → N < # LPT ∧ LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG)
;
{let empty? = ?
in {gc_heap_is_empty#(GCHEAP; empty?); if empty? then ERR := ENOSPC else {gc_heap_get_min#(GCHEAP; N); ERR := ESUCCESS}}
}
allocate-leb
: persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR)
{let AROFS0 = ?
in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0);
if AROFS0
then ERR := EROFS
else if FREELIST = []
then ERR := ENOSPC
else {N := FREELIST.head; awbuf_remap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL; ERR);
if ERR = ESUCCESS then {FREELIST := FREELIST.tail; LPT[N].size := 0; LPT[N].ref-size := 0}}}
}
;
allocate-gnd:
persistence_allocate_gnd#(WROOTADR, WMAXINO, WLPT, WORPHANS, AROFS; LOG, LPT, FREELIST, WLOG, WVOL, WBUFLEB; ERR)
precondition synced(WVOL);
postcondition true;
{if synced(WVOL)
then let N = ?
in {persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR);
if ERR = ESUCCESS
then {awbuf_add_log_leb#(N, 0, WROOTADR, WMAXINO, WVOL, WLPT, WORPHANS, AROFS; WLOG, WBUFLEB; ERR);
if ERR ≠ ESUCCESS then FREELIST := N + FREELIST};
if ERR = ESUCCESS then {LPT[N].flags := LP_GROUP_NODES; LOG := LOG + N}}
else abort
}
is-log-empty:persistence_is_log_empty#(LOG; ; EMPTY?) precondition true; postcondition true;{EMPTY? := LOG = []}
allocate-ind:
persistence_allocate_ind#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; LPT, FREELIST, WVOL, WBUFLEB; ERR)
precondition synced(WVOL);
postcondition true;
{if synced(WVOL)
then let N = ?
in {persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR);
if ERR = ESUCCESS
then {awbuf_move_buf#(N, 0, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR);
if ERR ≠ ESUCCESS then FREELIST := N + FREELIST else LPT[N].flags := LP_INDEX_NODES}}
else abort
}
deallocate-gnd:
persistence_deallocate_gnd#(N, LOG, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL; ERR)
precondition synced(WVOL) ∧ N < # LPT ∧ LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG;
postcondition true;
{if synced(WVOL) ∧ N < # LPT ∧ LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG
then let AROFS0 = ?
in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0);
if AROFS0
then ERR := EROFS
else {awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL); LPT[N].flags := LP_FREE;
LPT[N].ref-size := 0; LPT[N].size := 0; FREELIST := FREELIST + N; gc_heap_remove#(LPT[N].gcheapidx; GCHEAP, LPT);
ERR := ESUCCESS}}
else abort
}
sync:
persistence_sync#(LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; LPT, WVOL, AROFS; ERR)
precondition WBUFLEB.isbuf? ∧ ¬ AROFS
→ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].size ≤ LEB_SIZE ∧ WVOL[WBUFLEB.leb].mapped?
∧ LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data ∧ LPT[WBUFLEB.leb].flags ≠ LP_FREE
∧ is-aligned(LPT[WBUFLEB.leb].size, 2 * NODE_HEADER_SIZE)
;
postcondition true;
{if WBUFLEB.isbuf? ∧ ¬ AROFS
→ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].size ≤ LEB_SIZE ∧ WVOL[WBUFLEB.leb].mapped?
∧ LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data ∧ LPT[WBUFLEB.leb].flags ≠ LP_FREE
∧ is-aligned(LPT[WBUFLEB.leb].size, 2 * NODE_HEADER_SIZE)
then {ERR := ESUCCESS;
let WBUFLEB0 = ?, AROFS0 = ?, PAGESIZE = ?
in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0);
awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0);
awbuf_get_page_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; PAGESIZE);
if ¬ AROFS0
then if WBUFLEB0.isbuf?
then let OFFSET = LPT[WBUFLEB0.leb].size
in if ¬ is-aligned(OFFSET, PAGESIZE)
then let SIZE = PAGESIZE - OFFSET % PAGESIZE
in let BUF = mkbuf(SIZE)
in {persistence_encode_padding_node#(; BUF; ERR);
if ERR = ESUCCESS
then {awbuf_write_buf#
(# BUF, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR);
if ERR = ESUCCESS
then LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + SIZE
else {debug#("persistence: flushing of LEB " + WBUFLEB0.leb.toString + " failed");
LPT[WBUFLEB0.leb].size := LEBSIZE;
awbuf_enter_readonly#
(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}
else {debug#("persistence: could not encode padding node");
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}
else ERR := EROFS}}
else abort
}
encode-padding-node
: persistence_encode_padding_node#(; BUF; ERR)
{let SIZE = # BUF - 2 * NODE_HEADER_SIZE
in {encode_header#(nodeheader(SIZE, true), 0; BUF; ERR);
BUF := copy(validtrailer, 0, BUF, # BUF - NODE_HEADER_SIZE, NODE_HEADER_SIZE)}
}
;
cleanup-lpt
: persistence_cleanup_lpt#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL)
{let N = 0
in while N < # LPT
do {/* (prepost-cleanup-lpt
: invariant N ≤ # LPT ∧ # LPT = # LPT` ∧ id-idx(cleanup-lpt(LPT`, N), LPT) ∧ awbuf-inv(WVOL, WBUFLEB)
∧ avol-cleanup-lpt-unchanged(WVOL`, WVOL, LPT`) ∧ freelist-cons(LPT, FREELIST)
∧ keyset(GCHEAP) = gc-heap(cleanup-lpt(LPT`, N), []) ∧ bin-heap-inv(GCHEAP, LPT) ∧ WBUFLEB = nobuffer
∧ synced(WVOL)
wfbound # LPT - N)
*/;
if LPT[N].ref-size = 0 ∧ LPT[N].flags ≠ LP_FREE
then {if LPT[N].flags = LP_GROUP_NODES then gc_heap_remove#(LPT[N].gcheapidx; GCHEAP, LPT); LPT[N].flags := LP_FREE;
LPT[N].size := 0; FREELIST := FREELIST + N;
awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL)};
N := N + 1}
}
;
heap-add-log
: persistence_gc_heap_add_log#(; LOG, LPT, GCHEAP)
{while LOG ≠ []
do {/* (prepost-gcheap-add-log
: invariant bin-heap-inv(GCHEAP, LPT) ∧ keyset(GCHEAP) = gc-heap(LPT, LOG) ∧ id-idx(LPT`, LPT) ∧ ¬ dups(LOG)
∧ (∀ n. n ∈ LOG → n < # LPT ∧ LPT[n].flags = LP_GROUP_NODES)
wfbound # LOG)
*/;
let LNUM = LOG.head in let KI = key-index(LPT[LNUM].ref-size, LNUM) in gc_heap_insert#(KI; GCHEAP, LPT); LOG := LOG.tail}
}
;
commit:
persistence_commit#
(WROOTADR0, WMAXINO0; ORPHANS0, LOG, LPT, FREELIST, GCHEAP, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ERR)
precondition synced(WVOL);
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → WBUFLEB = nobuffer) ∧ (ERR = ESUCCESS ↔ ¬ AROFS);
{if synced(WVOL)
then {awbuf_destroy_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR);
if ERR = ESUCCESS
then awbuf_commit#(LPT, WROOTADR0, WMAXINO0, WVOL, WBUFLEB; ORPHANS0, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; ERR);
if ERR = ESUCCESS
then {persistence_gc_heap_add_log#(; LOG, LPT, GCHEAP);
persistence_cleanup_lpt#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL)}}
else abort
}
requires-commit:
persistence_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?)
precondition true;
postcondition true;
{awbuf_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?)
}
is-readonly:
persistence_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; ROFS)
precondition true;
postcondition true;
{awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; ROFS)
}
format:
persistence_format#
(VOLSIZE, SIZE, WMAXINO0; LPT, FREELIST, GCHEAP, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, LOG, LEBSIZE; ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {LPT := mklparray(VOLSIZE); LPT := fill(LPT, mklp(0, 0, LP_FREE, 0));
let ADR = @(0, 0, 0)
in awbuf_format#(VOLSIZE, SIZE, LPT, ADR, WMAXINO0; ; WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, ERR);
if ERR ≠ ESUCCESS
then debug#("persistence: wbuf format failed")
else {awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; LEBSIZE); LOG := [];
persistence_create_freelist#(LPT; FREELIST); gc_heap_empty#(; GCHEAP)}}
else abort
}
create-freelist
: persistence_create_freelist#(LPT; FREELIST)
{FREELIST := [];
let N = 0
in while N < # LPT
do {/* (prepost-create-freelist: invariant N ≤ # LPT ∧ freelist-cons(subarray(LPT, 0, N), FREELIST) wfbound # LPT - N)
*/;
if LPT[N].flags = LP_FREE then FREELIST := FREELIST + N; N := N + 1}
}
;
recover:
persistence_recover#
(; WROOTADR0, WMAXINO0, LOG0, ORPHANS, LOG, LPT, FREELIST, GCHEAP, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB,
AROFS
; ERR
)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ # WVOL = # WVOL` ∧ WROOTADR0 = WROOTADR ∧ WROOTADR = WROOTADR` ∧ WMAXINO0 = WMAXINO
∧ WMAXINO = WMAXINO` ∧ LOG0 = WLOG ∧ WLOG = WLOG` ∧ ORPHANS = WORPHANS ∧ WORPHANS = WORPHANS` ∧ WLPT = WLPT`
∧ WBUFLEB = nobuffer ∧ id-idx(replay-lpt(replay-log(WLPT, WLOG), WLOG, # WLPT), LPT))
;
{{awbuf_recover#(; WROOTADR0, WMAXINO0, ORPHANS, LOG0, LPT, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WVOL; WBUFLEB, AROFS, ERR);
LOG := LOG0;
if ERR ≠ ESUCCESS
then debug#("persistence: wbuf recover failed")
else {awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; LEBSIZE);
let LOG0 = LOG in persistence_replay_log#(LEBSIZE; LOG0, LPT);
persistence_replay_lpt#(LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, WVOL);
persistence_create_freelist#(LPT; FREELIST); persistence_create_gcheap#(LOG; LPT, GCHEAP)}}
}
replay-log
: persistence_replay_log#(LEBSIZE; LOG0, LPT)
{while LOG0 ≠ []
do {/* (prepost-replay-log
: invariant ∃ log. LOG0` = log + LOG0 ∧ LPT = replay-log(LPT`, log) ∧ valid-indices(LPT, LOG0`) ∧ ¬ dups(LOG0`)
wfbound # LOG0)
*/;
let N = LOG0.head in {LPT[N].flags := LP_GROUP_NODES; LPT[N].size := LEBSIZE; LOG0 := LOG0.tail}}
}
;
replay-lpt
: persistence_replay_lpt#(LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, WVOL)
{let N = 0
in while N < # LPT
do {/* (prepost-replay-lpt
: invariant N ≤ # LPT` ∧ awbuf-inv(WVOL, WBUFLEB) ∧ WBUFLEB = nobuffer ∧ LPT = replay-lpt(LPT`, LOG, N)
∧ # LPT` = # WVOL` ∧ avol-replay-lpt-unchanged(WVOL`, WVOL, LPT`, LOG) ∧ synced(WVOL)
wfbound # LPT - N)
*/;
if LPT[N].flags ≠ LP_FREE ∧ ¬ N ∈ LOG
then {if LPT[N].flags = LP_INDEX_NODES then LPT[N].size := LEBSIZE;
if LPT[N].ref-size = 0
then {LPT[N].flags := LP_FREE; LPT[N].size := 0;
awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL)}};
N := N + 1}
}
;
create-gcheap
: persistence_create_gcheap#(LOG; LPT, GCHEAP)
{gc_heap_empty#(; GCHEAP);
let N = 0
in while N < # LPT
do {/* (prepost-create-gcheap
: invariant N ≤ # LPT ∧ bin-heap-inv(GCHEAP, LPT) ∧ gc-heap(LPT, LOG, N) = keyset(GCHEAP) ∧ id-idx(LPT`, LPT)
wfbound # LPT - N)
*/;
if LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG
then let KI = key-index(LPT[N].ref-size, N) in gc_heap_insert#(KI; GCHEAP, LPT);
N := N + 1}
}
;
end data asm specification