[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
btree
using apersistence-asm
,
btree-inv, modification,
stringset
,
debug
procedures btree_index_contains#
key × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: bool × ref × zheap × index-store
: error
nondeterministic;
btree_index_lookup#
key × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: bool × address × ref × zheap × index-store
: error
nondeterministic;
btree_index_store#
key × address × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: address × bool × ref × zheap × index-store
nonfunctional
nondeterministic;
btree_index_remove#
key × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: address × bool × ref × zheap × index-store
nonfunctional
nondeterministic;
btree_index_truncate#
key × nat × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: address-set × ref × zheap × index-store
nonfunctional
nondeterministic;
btree_index_entries#
key × address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: stringset × ref × zheap
: error
nondeterministic;
btree_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;
btree_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;
btree_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;
btree_is_log_empty#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool
;
btree_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;
btree_sync#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set : persistence-state × bool : error
nondeterministic;
btree_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
;
btree_get_gblock_refsize#
nat × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: nat
;
btree_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;
btree_allocate_gnd#
address × index-store × index-store × group-store × nat × nat-set × bool : nat-set × group-store × nat-list × persistence-state : error
nondeterministic;
btree_deallocate_gnd#
nat × address × index-store × index-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: nat-set × group-store
: error
nondeterministic;
btree_requires_commit#
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
:
: bool
nondeterministic;
btree_get_leb_size
address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool : : nat
;
btree_format#
nat × nat × nat
: address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: ref × error
nondeterministic;
btree_recover#
: nat × nat-list × nat-set × address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat ×
nat-set × persistence-state × bool
: ref × error
nondeterministic;
btree_commit#
nat × ref
: nat-set × address × zheap × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: error
nondeterministic;
btree_commit_rec#
ref × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set
: address × error × zheap × index-store × persistence-state × bool
nonfunctional
nondeterministic;
btree_io_load#
ref × address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state ×
bool
: ref × zheap
: error
nondeterministic;
btree_io_save#
ref × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set
: address × zheap × index-store × persistence-state × bool
: error
nondeterministic;
btree_io_dirty#
ref × address × bool × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: error × zheap × index-store
nonfunctional
;
btree_io_scan# key × nat × ref × zheap : nat nonfunctional ;
btree_io_shift_left# nat × ref : zheap nonfunctional ;
btree_io_shift_n_left# nat × nat × ref : zheap nonfunctional ;
btree_io_shift_right# nat × ref : zheap nonfunctional ;
btree_io_split# nat × ref : ref × ref × error × zheap nonfunctional nondeterministic;
btree_traverse_root#
modification × ref × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: bool × bool × address × ref × zheap × index-store
: error
nondeterministic;
btree_traverse#
modification × ref × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × bool × bool × address × zheap × index-store
: error
nondeterministic;
btree_entries#
key × ref × address × address × index-store × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set ×
persistence-state × bool
: ref × bool × stringset × zheap
: error
nondeterministic;
btree_truncate#
key × ref × address × address × index-store × nat-set × group-store × group-store × nat-list × nat × nat-set × persistence-state × bool
: ref × bool × bool × address-set × zheap × index-store
: error
nondeterministic;
variables R : ref flexible;
R0 : ref flexible;
RN : ref flexible;
KEY : key flexible;
RT : ref flexible;
RP : ref flexible;
RC : ref flexible;
RL : ref flexible;
RR : ref flexible;
ADRT : address flexible;
ADRP : address flexible;
ADRC : address flexible;
ADR0 : address flexible;
ZH : zheap flexible;
DIRTY : bool flexible;
EXISTS : bool flexible;
FOUND : bool flexible;
SKIP : nat flexible;
POSITION : nat flexible;
SIZE : nat flexible;
M : nat flexible;
ND : node flexible;
ZND : znode flexible;
OLDADR : address flexible;
NAMES : stringset flexible;
DONE : bool flexible;
MOD : modification flexible;
AS : address-set flexible;
LEFT : nat flexible;
RIGHT : nat flexible;
NUSED : nat flexible;
LEAF : bool flexible;
GINVAL0 : nat-set flexible;
state variables RT : ref flexible;
ADRT : address flexible;
ZH : zheap flexible;
initialization procedure btree_format#
if ERR = ESUCCESS
sequential
invariants btree : ⊦ btree-inv(RT, ROOTADR, ISTORE, ISTORE0, ZH, RI, FI);
crash predicate true
recovery procedure btree_recover#
if ERR = ESUCCESS
declarations contains:
btree_index_contains#
(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; EXISTS, RT, ZH, ISTORE; ERR)
precondition true;
postcondition true;
{choose DIRTY, ADR
with true
in btree_traverse_root#
(contains(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; DIRTY, EXISTS, ADR, RT, ZH, ISTORE
; ERR)
}
lookup:
btree_index_lookup#
(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; EXISTS, ADR, RT, ZH, ISTORE; ERR)
precondition true;
postcondition true;
{choose DIRTY
with true
in btree_traverse_root#
(lookup(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; DIRTY, EXISTS, ADR, RT, ZH, ISTORE
; ERR)
}
store:
btree_index_store#
(KEY, ADR, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; OLDADR, EXISTS, RT, ZH, ISTORE)
precondition true;
postcondition true;
{choose DIRTY, ERR
with true
in btree_traverse_root#
(store(KEY, ADR), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; DIRTY, EXISTS, OLDADR, RT, ZH, ISTORE
; ERR)
}
remove:
btree_index_remove#
(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; OLDADR, EXISTS, RT, ZH, ISTORE)
precondition true;
postcondition true;
{choose DIRTY, ERR
with true
in btree_traverse_root#
(remove(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; DIRTY, EXISTS, OLDADR, RT, ZH, ISTORE
; ERR)
}
truncate:
btree_index_truncate#
(KEY, N, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; AS, RT, ZH, ISTORE)
precondition true;
postcondition true;
{let DIRTY = false, DONE = false, ERR = ?
in btree_truncate#
(datakey(KEY.ino, (N + VFS_PAGE_SIZE - 1) / VFS_PAGE_SIZE), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS,
PSTATE, PSYNCED
; RT, DIRTY, DONE, AS, ZH, ISTORE
; ERR)
}
entries:
btree_index_entries#
(KEY, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; NAMES, RT, ZH; ERR)
precondition true;
postcondition true;
{let DONE = false
in btree_entries#
(dentrykey(KEY.ino, ""), null, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; RT, DONE, NAMES, ZH
; ERR)
}
read-gnd:
btree_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 apersistence_read_gnd#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GND; ERR)
else abort
}
read-gblock:
btree_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 apersistence_read_gblock_nodes#
(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ADRLIST, GNDLIST; ERR)
else abort
}
get-gc-block:
btree_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR)
precondition true;
postcondition true;
{apersistence_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR)
}
is-log-empty:
btree_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?)
precondition true;
postcondition true;
{apersistence_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?)
}
add-gnds:
btree_add_gnds#(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR)
precondition NL ≠ [] ∧ PSTATE.journal?;
postcondition true;
{if NL ≠ [] ∧ PSTATE.journal?
then apersistence_add_gnds#
(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR)
else abort
}
sync:
btree_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)
precondition true;
postcondition true;
{apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)
}
set-gblock-refsize:
btree_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 apersistence_set_gblock_refsize#
(LNUM, N, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GSTORE)
else abort
}
get-gblock-refsize:
btree_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 apersistence_get_gblock_refsize#
(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
else abort
}
get-block-free-size:
btree_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition true;
postcondition true;
{apersistence_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
}
allocate-gnd:
btree_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR)
precondition PSYNCED;
postcondition true;
{if PSYNCED
then apersistence_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR)
else abort
}
deallocate-gnd:
btree_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 apersistence_deallocate_gnd#(N, ROOTADR, ISTORE, ISTORE0, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GINVAL, GSTORE; ERR)
else abort
}
requires-commit:
btree_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?)
precondition true;
postcondition true;
{apersistence_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?)
}
get-leb-size:
btree_get_leb_size(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
precondition true;
postcondition true;
{apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)
}
format:
btree_format#
(VOLSIZE, SIZE, MAXINO0; ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, ERR)
precondition SIZE = LEB_SIZE;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ btree-inv(RT, ROOTADR, ISTORE, ISTORE0, ZH, ∅, ∅) ∧ GSTORE = ∅ ∧ GINVAL = ∅ ∧ MAXINO = MAXINO0 ∧ NL = [] ∧ OS = ∅)
;
{if SIZE = LEB_SIZE
then {RT := null;
apersistence_format#
(VOLSIZE, SIZE, MAXINO0; ; ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED, ERR);
let N = ?
in {apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N);
if ERR = ESUCCESS
then let IND = indexnode(mkbrarray(BRANCH_SIZE), true, 0)
in let SIZE = IND.flashsize
in {if SIZE > N then {debug#("btree: initial index node to large"); ERR := ENOSPC};
if ERR = ESUCCESS
then apersistence_allocate_ind#
(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR);
if ERR = ESUCCESS
then apersistence_add_ind#
(IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADRT, ISTORE, PSTATE, PSYNCED; ERR);
if ERR = ESUCCESS
then apersistence_set_iblock_refsize#
(ADRT.lnum, SIZE, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE);
if ERR = ESUCCESS
then apersistence_sync#
(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR);
if ERR = ESUCCESS
then let NS = ∅
in apersistence_commit#
(ADRT, MAXINO0, PSYNCED
; NS, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS
; PSTATE, ERR)}}}
else abort
}
recover:
btree_recover#
(; MAXINO0, NL0, OS0, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, ERR)
precondition true;
postcondition true;
{{apersistence_recover#
(; ADRT, MAXINO0, NL0, OS0, ROOTADR, NL, MAXINO, OS, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0; PSTATE, PSYNCED, ERR);
RT := null}
}
commit:
btree_commit#(MAXINO0, RT; OS0, ADRT, ZH, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR)
precondition dom remove-refsize0(GSTORE) ∩ GINVAL = ∅ ∧ PSTATE = unbuffered ∧ ADRT = ROOTADR;
postcondition true;
{if dom remove-refsize0(GSTORE) ∩ GINVAL = ∅ ∧ PSTATE = unbuffered ∧ ADRT = ROOTADR
then {ERR := ESUCCESS;
let ADR = ADRT, DONE = false
in {if RT ≠ null ∧ ZH[RT].dirty
then {apersistence_allocate_ind#
(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR);
if ERR = ESUCCESS
then btree_commit_rec#
(RT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ERR, ZH, ISTORE, PSTATE, PSYNCED);
if ERR = ESUCCESS
then {DONE := true;
apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)}};
if ERR = ESUCCESS
then apersistence_commit#
(ADR, MAXINO0, PSYNCED; OS0, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS; PSTATE, ERR);
if ERR = ESUCCESS
then ADRT := ADR
else if DONE
then {ZH[RT].dirty := true;
let SIZE = 0
in {apersistence_get_iblock_refsize#
(ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE);
apersistence_set_iblock_refsize#
(ADR.lnum, SIZE - ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; ISTORE)}}}}
else abort
}
commit-rec
: btree_commit_rec#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ERR, ZH, ISTORE, PSTATE, PSYNCED)
{ERR := ESUCCESS;
if ¬ ZH[R].leaf
then let N = 0
in while N < ZH[R].usedsize ∧ ERR = ESUCCESS
do {let ADRC = ZH[R].zbranches[N].adr, RC = ZH[R].zbranches[N].child
in if RC ≠ null ∧ ZH[RC].dirty
then {btree_commit_rec#
(RC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADRC, ERR, ZH, ISTORE, PSTATE, PSYNCED);
if ERR = ESUCCESS then ZH[R].zbranches[N].adr := ADRC};
N := N + 1};
if ERR = ESUCCESS
then btree_io_save#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ZH, ISTORE, PSTATE, PSYNCED; ERR)
}
;
load
: btree_io_load#(R, ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RN, ZH; ERR)
{if RN = null
then let IND = ?
in {apersistence_read_ind#
(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; IND; ERR);
if ERR = ESUCCESS
then choose R0
with ¬ R0 ∈ ZH ∧ R0 ≠ null
in {ZH := ZH ++ R0; ZH[R0] := mkznode(R, mkzbrarray(BRANCH_SIZE), IND.leaf, false, IND.usedsize); RN := R0;
let N = 0 in while N < IND.usedsize do {ZH[RN].zbranches[N] := load(IND.branches[N]); N := N + 1}}
ifnone ERR := ENOMEM}
else ERR := ESUCCESS
}
;
io-save
: btree_io_save#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ZH, ISTORE, PSTATE, PSYNCED; ERR)
{let IND = save(ZH[R]), SIZE = 0
in {apersistence_get_block_free_size#
(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE);
if SIZE < IND.flashsize
then {apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR);
if ERR = ESUCCESS
then apersistence_allocate_ind#
(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR)}
else ERR := ESUCCESS;
if ERR = ESUCCESS
then {apersistence_add_ind#
(IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ISTORE, PSTATE, PSYNCED; ERR);
if ERR = ESUCCESS
then let SIZE = 0
in {apersistence_get_iblock_refsize#
(ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE);
apersistence_set_iblock_refsize#
(ADR.lnum, SIZE + ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)}}};
if ERR = ESUCCESS then ZH[R].dirty := false
}
;
dirty
: btree_io_dirty#(R, ADR, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE)
{if DIRTY
then {if ¬ ZH[R].dirty
then let SIZE = 0
in {apersistence_get_iblock_refsize#
(ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE);
apersistence_set_iblock_refsize#
(ADR.lnum, SIZE - ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)};
ZH[R].dirty := true}
}
;
scan
: btree_io_scan#(KEY, SKIP, R, ZH; POSITION)
{POSITION := 0; while POSITION + SKIP < ZH[R].usedsize ∧ ZH[R].zbranches[POSITION].key < KEY do POSITION := POSITION + 1}
;
shift-left
: btree_io_shift_left#(POSITION, R; ZH)
{let N = POSITION in while N + 1 < ZH[R].usedsize do ZH[R].zbranches[N] := ZH[R].zbranches[N + 1], N := N + 1}
;
shift-n-left
: btree_io_shift_n_left#(POSITION, N, R; ZH)
{let M = POSITION in while M + N < ZH[R].usedsize do ZH[R].zbranches[M] := ZH[R].zbranches[M + N], M := M + 1}
;
shift-right
: btree_io_shift_right#(POSITION, R; ZH)
{let N = ZH[R].usedsize in while POSITION < N do ZH[R].zbranches[N] := ZH[R].zbranches[N - 1], N := N - 1}
;
split
: btree_io_split#(POSITION, R; RL, RR, ERR, ZH)
{let NUSED = ZH[R].usedsize
in let LEFT = POSITION, RIGHT = NUSED - POSITION, RP = ZH[R].parent, LEAF = ZH[R].leaf, DIRTY = ZH[R].dirty
in choose R0
with ¬ R0 ∈ ZH ∧ R0 ≠ null
in {ZH := ZH ++ R0; ZH[R0] := mkznode(RP, mkzbrarray(BRANCH_SIZE), LEAF, DIRTY, RIGHT); RR := R0; RL := R;
ZH[RL].usedsize := LEFT;
let N = 0 in while N < RIGHT do ZH[RR].zbranches[N] := ZH[RL].zbranches[POSITION + N], N := N + 1;
ZH[RL].dirty := true; ZH[RR].dirty := true; ERR := ESUCCESS}
ifnone ERR := ENOMEM
}
;
traverse-root
: btree_traverse_root#
(MOD, RP, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; DIRTY, EXISTS, ADR, RT, ZH, ISTORE; ERR)
{btree_traverse#
(MOD, RP, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR);
if ERR = ESUCCESS
then if ZH[RT].usedsize = BRANCH_SIZE
then let RL = null, RR = null, POSITION = MIN_SIZE
in {btree_io_split#(POSITION, RT; RL, RR, ERR, ZH);
choose R
with ¬ R ∈ ZH ∧ R ≠ null
in {ZH := ZH ++ R; ZH[R] := mkznode(null, mkzbrarray(BRANCH_SIZE), false, true, 2); RT := R; DIRTY := true};
let KEY = ZH[RL].zbranches[POSITION - 1].key
in {ZH[RL].parent := RT; ZH[RR].parent := RT; ZH[RT].zbranches[0] := mkzbranch(KEY, ADRT, RL);
ZH[RT].zbranches[1] := mkzbranch(KEY, ADRT, RR)}}
}
;
traverse
: btree_traverse#
(MOD, RP, ADR0, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR)
{btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR);
if ERR = ESUCCESS
then {if ZH[R].leaf
then let N = 0
in {btree_io_scan#(MOD.key, 0, R, ZH; N);
let FOUND = N < ZH[R].usedsize ∧ ZH[R].zbranches[N].key = MOD.key
in {EXISTS := FOUND ∧ ZH[R].zbranches[N].entry?; if EXISTS then ADR := ZH[R].zbranches[N].adr;
if MOD.contains?
then {ERR := ESUCCESS; DIRTY := false}
else if MOD.lookup?
then {ERR := ESUCCESS; DIRTY := false}
else if MOD.store?
then {if ¬ FOUND then {btree_io_shift_right#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize + 1};
ZH[R].zbranches[N] := mkzentry(MOD.key, MOD.adr); DIRTY := true; ERR := ESUCCESS}
else if MOD.remove?
then if FOUND
then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1;
DIRTY := true; ERR := ESUCCESS}
else {DIRTY := false; ERR := ESUCCESS}}}
else let N = 0
in {btree_io_scan#(MOD.key, 1, R, ZH; N);
let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr
in {btree_traverse#
(MOD, R, ADRC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; RC, DIRTY, EXISTS, ADR, ZH, ISTORE
; ERR);
if ERR = ESUCCESS
then if ZH[RC].usedsize = BRANCH_SIZE
then let RL = null, RR = null, POSITION = MIN_SIZE
in {btree_io_split#(POSITION, RC; RL, RR, ERR, ZH); btree_io_shift_right#(N, R; ZH);
ZH[R].zbranches[N].child := RL; ZH[R].zbranches[N].key := ZH[RL].zbranches[POSITION - 1].key;
ZH[R].zbranches[N + 1].child := RR; ZH[R].usedsize := ZH[R].usedsize + 1; DIRTY := true}
else if ZH[RC].usedsize = 0 ∧ ZH[R].usedsize ≠ 0
then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; DIRTY := true;
ZH := ZH -- RC}
else ZH[R].zbranches[N].child := RC}};
btree_io_dirty#
(R, ADR0, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE)}
}
;
btree-entries
: btree_entries#
(KEY, RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DONE, NAMES, ZH; ERR)
{btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR);
if ERR = ESUCCESS
then if ZH[R].leaf
then let N = 0
in {btree_io_scan#(KEY, 0, R, ZH; N);
while N < ZH[R].usedsize ∧ KEY.ino = ZH[R].zbranches[N].key.ino ∧ ZH[R].zbranches[N].key.dentry?
do {NAMES := NAMES ++ ZH[R].zbranches[N].key.name; N := N + 1};
DONE := N < ZH[R].usedsize}
else let N = 0
in {btree_io_scan#(KEY, 1, R, ZH; N);
while N < ZH[R].usedsize ∧ ¬ DONE
do let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr
in {btree_entries#
(KEY, R, ADRC, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; RC, DONE, NAMES, ZH
; ERR);
N := N + 1}}
}
;
btree-truncate
: btree_truncate#
(KEY, RP, ADR0, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DIRTY, DONE, AS, ZH, ISTORE; ERR)
{btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR);
if ERR = ESUCCESS
then if ZH[R].leaf
then let POSITION = 0, N = 0
in {btree_io_scan#(KEY, 0, R, ZH; POSITION);
while POSITION + N < ZH[R].usedsize ∧ KEY.ino = ZH[R].zbranches[POSITION + N].key.ino
∧ ZH[R].zbranches[POSITION + N].key.data?
do {if ZH[R].zbranches[POSITION + N].entry? then AS := AS ++ ZH[R].zbranches[POSITION + N].adr; DIRTY := true;
N := N + 1};
btree_io_shift_n_left#(POSITION, N, R; ZH); DONE := POSITION + N < ZH[R].usedsize;
ZH[R].usedsize := ZH[R].usedsize - N}
else let N = 0
in {btree_io_scan#(KEY, 1, R, ZH; N);
while N < ZH[R].usedsize ∧ ¬ DONE
do let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr
in {btree_truncate#
(KEY, R, ADRC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED
; RC, DIRTY, DONE, AS, ZH, ISTORE
; ERR);
ZH[R].zbranches[N].child := RC;
if ZH[RC].usedsize = 0 ∧ ZH[R].usedsize ≠ 0
then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; ZH := ZH -- RC}
else N := N + 1}};
btree_io_dirty#(R, ADR0, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE)
}
;
end data asm specification