[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_io
using ebm-avol-asm
,
persistence-io-inv
procedures persistence_io_commit# lp-array × address × nat × nat × nat : nat-set × superblock × avolume × nat : error nondeterministic;
persistence_io_requires_commit# nat × nat : : bool ;
persistence_io_add_log_leb# nat × superblock × nat × nat : nat × avolume : error nondeterministic;
persistence_io_read_log# superblock × nat × nat × avolume : nat : nat-list × error nondeterministic;
persistence_io_write_superblock# superblock × nat × nat : avolume : error nondeterministic;
persistence_io_read_superblock# nat × nat × avolume : superblock : error nondeterministic;
persistence_io_encode_lpt# lp-array × nat : : buffer × error nondeterministic;
persistence_io_decode_lpt# buffer : lp-array × error nonfunctional nondeterministic;
persistence_io_write_lebs# nat × nat × buffer × nat : avolume : error nondeterministic;
persistence_io_read_lebs# nat × nat × nat × avolume : : buffer × error nondeterministic;
persistence_io_encode_orphans# nat × nat : nat-set × buffer : error nondeterministic;
persistence_io_decode_orphans# nat × buffer : : nat-set × error nondeterministic;
persistence_io_read_orphans# superblock × avolume : nat-set : error nondeterministic;
persistence_io_write_orphans# nat × nat × nat : nat-set × avolume : error nondeterministic;
persistence_io_get_page_size# nat : : nat ;
persistence_io_get_leb_size# nat : : nat ;
persistence_io_format# nat × nat × lp-array × address × nat : superblock × nat × nat × avolume : nat × error nondeterministic;
persistence_io_recover# : address × nat × nat-set × nat-list × lp-array × superblock × nat × nat × nat × avolume : error
nondeterministic;
persistence_io_get_volume_size# superblock × avolume : : nat ;
persistence_io_write# nat × nat × nat × nat × buffer × superblock : avolume : error nondeterministic;
persistence_io_read# nat × nat × nat × nat × superblock × avolume : buffer : error nondeterministic;
persistence_io_remap# nat × superblock : avolume : error nondeterministic;
persistence_io_unmap# nat × superblock : avolume nonfunctional ;
variables SB : superblock flexible;
NEWSB : superblock flexible;
INDEXADR : address flexible;
INDEXADR0 : address flexible;
MAXINO : nat flexible;
MAXINO0 : nat flexible;
LOGOFF : nat flexible;
SIZE : nat flexible;
COMMIT? : bool flexible;
LOG : nat-list flexible;
RND : ref-node flexible;
log : nat-list;
LPT : lp-array flexible;
ORPHANS : nat-set flexible;
LEBSIZE : nat flexible;
PAGESIZE : nat flexible;
state variables SB : superblock flexible;
LOGOFF : nat flexible;
PAGESIZE : nat flexible;
LEBSIZE : nat flexible;
initialization procedure persistence_io_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ ∃ LPT, LOG, ORPHANS. persistence-io-inv(SB, LOGOFF, AVOL, LPT, LOG, ORPHANS);
pagesize : ⊦ PAGESIZE = EB_PAGE_SIZE;
lebsize : ⊦ LEBSIZE = LEB_SIZE;
recovery procedure persistence_io_recover#
if ERR = ESUCCESS
declarations commit:
persistence_io_commit#(LPT, INDEXADR0, MAXINO0, PAGESIZE, LEBSIZE; ORPHANS, SB, AVOL, LOGOFF; ERR)
precondition # LPT + SB.main = # AVOL;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ SB.indexaddr = INDEXADR0 ∧ SB.maxino = MAXINO0 ∧ is-encoded([], AVOL[SB.log].data)
∧ is-encoded(LPT, lebs(AVOL, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE)))
∧ is-encoded-pad(ORPHANS`, SB.orphsize, AVOL[SB.orph].data))
∧ ( ERR ≠ ESUCCESS
→ SB = SB` ∧ AVOL[SB.log] = (AVOL`)[SB.log] ∧ AVOL[SB.orph] = (AVOL`)[SB.orph]
∧ lebs(AVOL, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE))
= lebs(AVOL`, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE)))
∧ SB.main = SB`.main ∧ # AVOL = # AVOL`
∧ subarray(AVOL, SB.main, # AVOL - SB.main) = subarray(AVOL`, SB.main, # AVOL - SB.main)
;
{if # LPT + SB.main = # AVOL
then let VOLSIZE = ?
in {ebm_avol_get_volume_size#(AVOL; ; VOLSIZE); VOLSIZE := VOLSIZE - SB.main;
let NEWSB = SB
in {NEWSB.indexaddr := INDEXADR0; NEWSB.maxino := MAXINO0; NEWSB.orphsize := # ORPHANS;
if NEWSB.log = SB_LOG
then {NEWSB.log := SB_LOG + 1; NEWSB.orph := SB_ORPH + 1; NEWSB.lpt := SB_LPT + lptlebs(VOLSIZE, LEBSIZE)}
else {NEWSB.log := SB_LOG; NEWSB.orph := SB_ORPH; NEWSB.lpt := SB_LPT};
ebm_avol_remap#(NEWSB.log; AVOL; ERR);
if ERR = ESUCCESS then persistence_io_write_orphans#(NEWSB.orph, PAGESIZE, LEBSIZE; ORPHANS, AVOL; ERR);
if ERR = ESUCCESS
then let BUF = ?
in {persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR);
if ERR = ESUCCESS
then persistence_io_write_lebs#(NEWSB.lpt, lptlebs(VOLSIZE, LEBSIZE), BUF, LEBSIZE; AVOL; ERR)};
if ERR = ESUCCESS then ebm_avol_sync_device#(AVOL; ; ERR);
if ERR = ESUCCESS then persistence_io_write_superblock#(NEWSB, PAGESIZE, LEBSIZE; AVOL; ERR);
if ERR = ESUCCESS then {SB := NEWSB; LOGOFF := 0}}}
else abort
}
requires-commit:
persistence_io_requires_commit#(LOGOFF, LEBSIZE; ; COMMIT?)
precondition true;
postcondition true;
{COMMIT? := LOGOFF = LEBSIZE
}
add-log-leb:
persistence_io_add_log_leb#(LNUM, SB, PAGESIZE, LEBSIZE; LOGOFF, AVOL; ERR)
precondition true;
postcondition true;
{if ¬ LOGOFF + PAGESIZE ≤ LEBSIZE
then ERR := ECOMMIT
else let BUF = mkbuf(PAGESIZE)
in {encode_ref_node#(PAGESIZE, rnode(LNUM); BUF; ERR);
if ERR = ESUCCESS
then {ebm_avol_write#(SB.log, LOGOFF, 0, PAGESIZE, BUF; AVOL; ERR);
if ERR = ESUCCESS
then LOGOFF := LOGOFF + PAGESIZE
else {LOGOFF := LEBSIZE; debug#("persistence-io: failed to add LEB " + LNUM.toString + " to log")}}}
}
read-log
: persistence_io_read_log#(SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF; LOG, ERR)
{LOG := []; ERR := ESUCCESS; LOGOFF := 0;
let BUF = mkbuf(PAGESIZE)
in while ERR = ESUCCESS ∧ LOGOFF < LEBSIZE
do {/* (prepost-read-log
: invariant LOGOFF ≤ LEB_SIZE ∧ # BUF = PAGESIZE ∧ is-aligned(LOGOFF, PAGESIZE)
∧ (ERR = ESUCCESS ∨ ERR = ENOENT ∨ ⌊ERR⌋ ) ∧ ebm-vol-inv(AVOL) ∧ SB.log < # AVOL
∧ AVOL[SB.log].mapped?
∧ ( ERR = ESUCCESS
→ LOGOFF ≤ # AVOL[SB.log].data ∧ is-encoded(LOG, subarray(AVOL[SB.log].data, 0, LOGOFF)))
∧ (ERR = ENOENT → is-encoded(LOG, AVOL[SB.log].data))
wfbound LEB_SIZE - LOGOFF)
*/;
ebm_avol_read#(SB.log, LOGOFF, 0, PAGESIZE, AVOL; BUF; ERR);
if ERR = ESUCCESS
then if isempty(BUF)
then ERR := ENOENT
else let RND = ? in {decode_ref_node#(PAGESIZE, BUF; RND; ERR); if ERR = ESUCCESS then LOG := LOG + RND.leb};
LOGOFF := LOGOFF + PAGESIZE};
if ERR = ENOENT then ERR := ESUCCESS
}
;
write-superblock
: persistence_io_write_superblock#(NEWSB, PAGESIZE, LEBSIZE; AVOL; ERR)
{let SIZE = encoding-size(NEWSB, PAGESIZE)
in if SIZE ≤ LEBSIZE
then let BUF = mkbuf(SIZE)
in {encode_superblock#(NEWSB, 0, PAGESIZE; BUF, SIZE; ERR);
if ERR = ESUCCESS then ebm_avol_change#(0, SIZE, BUF; AVOL; ERR)}
else ERR := ENOSPC
}
;
read-superblock
: persistence_io_read_superblock#(PAGESIZE, LEBSIZE, AVOL; NEWSB; ERR)
{let BUF = mkbuf(LEBSIZE)
in {ebm_avol_read#(0, 0, 0, LEBSIZE, AVOL; BUF; ERR);
if ERR = ESUCCESS then let SIZE = ? in decode_superblock#(0, BUF, PAGESIZE; NEWSB, SIZE; ERR)}
}
;
encode-lpt
: persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR)
{ERR := ESUCCESS; BUF := mkbuf(lptsize(# LPT, LEBSIZE));
let N = 0, SIZE = ?
in while ERR = ESUCCESS ∧ N < # LPT
do {/* (prepost-encode-lpt
: invariant N ≤ # LPT ∧ # BUF = lptsize(# LPT, LEB_SIZE) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ (ERR = ESUCCESS → is-encoded(LPT, BUF, N))
wfbound # LPT - N)
*/;
encode_lprops#(LPT[N], N * ENCODED_LPROPS_SIZE; BUF, SIZE; ERR); N := N + 1}
}
;
decode-lpt
: persistence_io_decode_lpt#(BUF; LPT, ERR)
{ERR := ESUCCESS;
let N = 0
in while ERR = ESUCCESS ∧ N < # LPT
do {/* (prepost-decode-lpt
: invariant N ≤ # LPT ∧ # BUF = lptsize(# LPT, LEB_SIZE) ∧ # LPT = # LPT`
∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → is-encoded(LPT, BUF, N))
wfbound # LPT - N)
*/;
let SIZE = ? in decode_lprops#(N * ENCODED_LPROPS_SIZE, BUF; LPT[N], SIZE; ERR); N := N + 1}
}
;
write-lebs
: persistence_io_write_lebs#(LNUM, SIZE, BUF, LEBSIZE; AVOL; ERR)
{ERR := ESUCCESS;
let N = 0
in while ERR = ESUCCESS ∧ N < SIZE
do {/* (prepost-write-lebs
: invariant N ≤ SIZE ∧ ebm-vol-inv(AVOL) ∧ # BUF = SIZE * LEB_SIZE ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ # AVOL = # AVOL` ∧ range=(AVOL, 0, AVOL`, 0, LNUM)
∧ range=(AVOL, LNUM + SIZE, AVOL`, LNUM + SIZE, # AVOL` - LNUM + SIZE)
∧ (ERR = ESUCCESS → lebs(AVOL, LNUM, N) = subarray(BUF, 0, N * LEB_SIZE) ∧ mapped-full?(AVOL, LNUM, N))
wfbound SIZE - N)
*/;
ebm_avol_remap#(LNUM + N; AVOL; ERR);
if ERR = ESUCCESS then ebm_avol_write#(LNUM + N, 0, N * LEBSIZE, LEBSIZE, BUF; AVOL; ERR); N := N + 1}
}
;
read-lebs
: persistence_io_read_lebs#(LNUM, SIZE, LEBSIZE, AVOL; ; BUF, ERR)
{ERR := ESUCCESS; BUF := mkbuf(SIZE * LEBSIZE);
let N = 0
in while ERR = ESUCCESS ∧ N < SIZE
do {/* (prepost-read-lebs
: invariant N ≤ SIZE ∧ # BUF = SIZE * LEB_SIZE ∧ LNUM + SIZE ≤ # AVOL ∧ ebm-vol-inv(AVOL)
∧ mapped-full?(AVOL, LNUM, SIZE) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ (ERR = ESUCCESS → subarray(BUF, 0, N * LEB_SIZE) = lebs(AVOL, LNUM, N))
wfbound SIZE - N)
*/;
ebm_avol_read#(LNUM + N, 0, N * LEBSIZE, LEBSIZE, AVOL; BUF; ERR); N := N + 1}
}
;
encode-orphans
: persistence_io_encode_orphans#(PAGESIZE, LEBSIZE; ORPHANS, BUF; ERR)
{if # ORPHANS * ENCODED_NAT_SIZE > LEBSIZE
then ERR := ENOSPC
else {ERR := ESUCCESS; BUF := mkbuf(align↑(# ORPHANS * ENCODED_NAT_SIZE, PAGESIZE));
let OFFSET = 0, SIZE = ?
in while ERR = ESUCCESS ∧ ORPHANS ≠ ∅
do {/* (prepost-encode-orphans
: invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ is-aligned(# BUF, PAGESIZE) ∧ ORPHANS ⊆ ORPHANS`
∧ # BUF ≤ LEBSIZE
∧ ( ERR = ESUCCESS
→ OFFSET + # ORPHANS * ENCODED_NAT_SIZE ≤ # BUF
∧ is-encoded(ORPHANS` \ ORPHANS, subarray(BUF, 0, OFFSET)))
wfbound # ORPHANS)
*/;
choose N
with N ∈ ORPHANS
in {encode_nat#(N, OFFSET; BUF, SIZE; ERR); OFFSET := OFFSET + ENCODED_NAT_SIZE; ORPHANS := ORPHANS -- N}}}
}
;
decode-orphans
: persistence_io_decode_orphans#(SIZE, BUF; ; ORPHANS, ERR)
{ORPHANS := ∅; ERR := ESUCCESS;
let OFFSET = 0
in while ERR = ESUCCESS ∧ SIZE ≠ 0
do {/* (prepost-decode-orphans
: invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ OFFSET + SIZE * ENCODED_NAT_SIZE = # BUF
∧ ( ERR = ESUCCESS
→ (∃ orphans.
is-encoded(ORPHANS, subarray(BUF, 0, OFFSET))
∧ is-encoded(orphans, subarray(BUF, OFFSET, # BUF - OFFSET)) ∧ orphans ∩ ORPHANS = ∅))
wfbound SIZE)
*/;
let N = ?, SIZE = ?
in {decode_nat#(OFFSET, BUF; N, SIZE; ERR); if ERR = ESUCCESS then ORPHANS := ORPHANS ++ N;
OFFSET := OFFSET + ENCODED_NAT_SIZE};
SIZE := SIZE - 1}
}
;
read-orphans
: persistence_io_read_orphans#(SB, AVOL; ORPHANS; ERR)
{let BUF = mkbuf(SB.orphsize * ENCODED_NAT_SIZE)
in {ebm_avol_read#(SB.orph, 0, 0, SB.orphsize * ENCODED_NAT_SIZE, AVOL; BUF; ERR);
if ERR = ESUCCESS then persistence_io_decode_orphans#(SB.orphsize, BUF; ; ORPHANS, ERR)}
}
;
write-orphans
: persistence_io_write_orphans#(LNUM, PAGESIZE, LEBSIZE; ORPHANS, AVOL; ERR)
{let BUF = mkbuf(0)
in {persistence_io_encode_orphans#(PAGESIZE, LEBSIZE; ORPHANS, BUF; ERR);
if ERR = ESUCCESS then ebm_avol_remap#(LNUM; AVOL; ERR);
if ERR = ESUCCESS then ebm_avol_write#(LNUM, 0, 0, # BUF, BUF; AVOL; ERR)}
}
;
get-page-size:persistence_io_get_page_size#(PAGESIZE; ; N) precondition true; postcondition true;{N := PAGESIZE}
get-leb-size:persistence_io_get_leb_size#(LEBSIZE; ; N) precondition true; postcondition true;{N := LEBSIZE}
format:
persistence_io_format#(VOLSIZE, SIZE, LPT, INDEXADR0, MAXINO0; SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF, ERR)
precondition VOLSIZE = # LPT ∧ SIZE = LEB_SIZE;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ SB.indexaddr = INDEXADR0 ∧ SB.maxino = MAXINO0
∧ subarray(AVOL, SB.main, # AVOL - SB.main) = fill(mkavolume(VOLSIZE), unmapped)
∧ is-encoded(LPT, lebs(AVOL, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE)))
∧ is-encoded([], AVOL[SB.log].data) ∧ is-encoded(∅, AVOL[SB.orph].data))
;
{if VOLSIZE = # LPT ∧ SIZE = LEB_SIZE
then let N = 5 + 2 * lptlebs(VOLSIZE, SIZE)
in {ebm_avol_format#(VOLSIZE + N; ; AVOL, ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: ubi format failed");
if ERR = ESUCCESS then ebm_avol_get_leb_size#(AVOL; ; LEBSIZE); SB.indexaddr := INDEXADR0; SB.maxino := MAXINO0;
SB.log := SB_LOG; SB.orph := SB_ORPH; SB.orphsize := 0; SB.lpt := SB_LPT; SB.main := N;
if ERR = ESUCCESS then ebm_avol_get_page_size#(AVOL; ; PAGESIZE);
if ERR = ESUCCESS then ebm_avol_remap#(SB.log; AVOL; ERR);
if ERR = ESUCCESS then ebm_avol_remap#(SB.orph; AVOL; ERR);
if ERR = ESUCCESS
then let BUF = ?
in {persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR);
if ERR = ESUCCESS then persistence_io_write_lebs#(SB.lpt, lptlebs(VOLSIZE, LEBSIZE), BUF, LEBSIZE; AVOL; ERR)};
if ERR = ESUCCESS then persistence_io_write_superblock#(SB, PAGESIZE, LEBSIZE; AVOL; ERR); LOGOFF := LEBSIZE}
else abort
}
recover:
persistence_io_recover#(; INDEXADR0, MAXINO0, ORPHANS, LOG, LPT, SB, LOGOFF, PAGESIZE, LEBSIZE, AVOL; ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ SB = SB` ∧ # AVOL = # AVOL` ∧ INDEXADR0 = SB.indexaddr ∧ MAXINO0 = SB.maxino
∧ # LPT = # AVOL - SB.main ∧ is-encoded(LPT, lebs(AVOL, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE)))
∧ lebs(AVOL, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE))
= lebs(AVOL`, SB.lpt, lptlebs(# AVOL - SB.main, LEB_SIZE))
∧ is-encoded(LOG, AVOL[SB.log].data) ∧ is-encoded-pad(ORPHANS, SB.orphsize, AVOL[SB.orph].data)
∧ AVOL[SB.orph] = (AVOL`)[SB.orph] ∧ AVOL[SB.log] = (AVOL`)[SB.log])
;
{{ebm_avol_recover#(; AVOL; ERR);
if ERR ≠ ESUCCESS
then debug#("persistence-io: ubi recover failed")
else let VOLSIZE = ?
in {ebm_avol_get_leb_size#(AVOL; ; LEBSIZE); ebm_avol_get_page_size#(AVOL; ; PAGESIZE);
ebm_avol_get_volume_size#(AVOL; ; VOLSIZE); persistence_io_read_superblock#(PAGESIZE, LEBSIZE, AVOL; SB; ERR);
if ERR ≠ ESUCCESS then debug#("persistence-io: reading superblock failed");
if ERR = ESUCCESS
then {persistence_io_read_log#(SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF; LOG, ERR);
if ERR ≠ ESUCCESS then debug#("persistence-io: reading log failed")};
if ERR = ESUCCESS
then {persistence_io_read_orphans#(SB, AVOL; ORPHANS; ERR);
if ERR ≠ ESUCCESS then debug#("persistence-io: reading orphans failed")};
if ERR = ESUCCESS
then {VOLSIZE := VOLSIZE - SB.main;
let BUF = ?
in {persistence_io_read_lebs#(SB.lpt, lptlebs(VOLSIZE, LEBSIZE), LEBSIZE, AVOL; ; BUF, ERR);
if ERR = ESUCCESS
then {LPT := mklparray(VOLSIZE); LPT := fill(LPT, mklp(0, 0, LP_FREE, 0));
persistence_io_decode_lpt#(BUF; LPT, ERR)};
if ERR ≠ ESUCCESS then debug#("persistence-io: reading LPT failed")}};
if ERR = ESUCCESS then {LOGOFF := LEBSIZE; INDEXADR0 := SB.indexaddr; MAXINO0 := SB.maxino}}}
}
get-volume-size:
persistence_io_get_volume_size#(SB, AVOL; ; N)
precondition true;
postcondition true;
{{ebm_avol_get_volume_size#(AVOL; ; N); N := N - SB.main}
}
write:
persistence_io_write#(LNUM, OFFSET, N0, N, BUF, SB; AVOL; ERR)
precondition SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ # AVOL[SB.main + LNUM].data ≤ OFFSET
∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
;
postcondition true;
{if SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ # AVOL[SB.main + LNUM].data ≤ OFFSET
∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
then ebm_avol_write#(SB.main + LNUM, OFFSET, N0, N, BUF; AVOL; ERR)
else abort
}
read:
persistence_io_read#(LNUM, OFFSET, N0, N, SB, AVOL; BUF; ERR)
precondition SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE;
postcondition true;
{if SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE
then ebm_avol_read#(SB.main + LNUM, OFFSET, N0, N, AVOL; BUF; ERR)
else abort
}
remap:
persistence_io_remap#(LNUM, SB; AVOL; ERR)
precondition SB.main + LNUM < # AVOL;
postcondition true;
{if SB.main + LNUM < # AVOL then ebm_avol_remap#(SB.main + LNUM; AVOL; ERR) else abort
}
unmap:
persistence_io_unmap#(LNUM, SB; AVOL)
precondition SB.main + LNUM < # AVOL;
postcondition true;
{if SB.main + LNUM < # AVOL then ebm_avol_unmap#(SB.main + LNUM; AVOL) else abort
}
end data asm specification