[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
wbuf
using wbuf-base,
apersistence-io-asm
procedures wbuf_get_buf# bufleb : : bufleb ;
wbuf_is_readonly# bool : : bool ;
wbuf_enter_readonly# : : bool ;
wbuf_move_buf# nat × nat × bool × avolume : bufleb × wbuf : error ;
wbuf_destroy_buf# bool : bufleb : error ;
wbuf_write_buf# nat × buffer × bufleb × nat × address × nat × nat-list × lp-array × nat-set : wbuf × bool × avolume : error
nondeterministic;
wbuf_read_buf# nat × nat × nat × bufleb × wbuf × address × nat × nat-list × avolume × lp-array × nat-set : buffer : error
nondeterministic;
wbuf_get_volume_size# address × nat × nat-list × avolume × lp-array × nat-set : : nat ;
wbuf_commit# lp-array × address × nat × avolume : nat-set × address × nat × nat-list × lp-array × nat-set × bool : error
nondeterministic;
wbuf_requires_commit# address × nat × nat-list × avolume × lp-array × nat-set : : bool nondeterministic;
wbuf_add_log_leb# nat × nat × bool × address × nat × avolume × lp-array × nat-set : bufleb × wbuf × nat-list : error
nondeterministic;
wbuf_remap# nat × bufleb × address × nat × nat-list × lp-array × nat-set : avolume : error nondeterministic;
wbuf_unmap# nat × bufleb × address × nat × nat-list × lp-array × nat-set : avolume nonfunctional ;
wbuf_get_page_size# nat : : nat ;
wbuf_get_leb_size# address × nat × nat-list × avolume × lp-array × nat-set : : nat ;
wbuf_format#
nat × nat × lp-array × address × nat : wbuf × nat × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : error
nondeterministic;
wbuf_recover#
: address × nat × nat-set × nat-list × lp-array × wbuf × nat × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool
: error
nondeterministic;
variables WROOTADR : address flexible;
WMAXINO : nat flexible;
WLOG : nat-list flexible;
WVOL : avolume flexible;
WLPT : lp-array flexible;
WORPHANS : nat-set flexible;
BUFLEB : bufleb flexible;
BUFLEB0 : bufleb flexible;
WBUF : wbuf flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
N2 : nat flexible;
LNUM : nat flexible;
OFFSET : nat flexible;
VOLSIZE : nat flexible;
PAGESIZE : nat flexible;
ROFS : bool flexible;
ROFS0 : bool flexible;
BEGINWBUF : nat flexible;
BEGINBUF : nat flexible;
state variables BUFLEB : bufleb flexible;
WBUF : wbuf flexible;
ROFS : bool flexible;
PAGESIZE : nat flexible;
initialization procedure wbuf_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ wbuf-cons(BUFLEB, WBUF, PVOL, ROFS);
pagesize : ⊦ PAGESIZE = EB_PAGE_SIZE;
recovery procedure wbuf_recover#
if ERR = ESUCCESS
declarations get-buf:wbuf_get_buf#(BUFLEB; ; BUFLEB0) precondition true; postcondition true;{BUFLEB0 := BUFLEB}
is-readonly:wbuf_is_readonly#(ROFS; ; ROFS0) precondition true; postcondition true;{ROFS0 := ROFS}
enter-readonly:wbuf_enter_readonly#(; ; ROFS) precondition true; postcondition true;{ROFS := true}
move-buf:
wbuf_move_buf#(LNUM, OFFSET, ROFS, PVOL; BUFLEB, WBUF; ERR)
precondition ¬ ROFS
→ BUFLEB = buffered(LNUM)
∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data
;
postcondition true;
{if ¬ ROFS
→ BUFLEB = buffered(LNUM)
∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data
then if ROFS
then ERR := EROFS
else {ERR := ESUCCESS; if BUFLEB ≠ buffered(LNUM) then {BUFLEB := buffered(LNUM); WBUF.offset := OFFSET; WBUF.nbytes := 0}}
else abort
}
destroy-buf:
wbuf_destroy_buf#(ROFS; BUFLEB; ERR)
precondition true;
postcondition true;
{if ROFS then ERR := EROFS else {BUFLEB := nobuffer; ERR := ESUCCESS}
}
write-buf:
wbuf_write_buf#(N, BUF, BUFLEB, PAGESIZE, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; WBUF, ROFS, PVOL; ERR)
precondition BUFLEB ≠ nobuffer ∧ (¬ ROFS → WBUF.offset + WBUF.nbytes + N ≤ LEB_SIZE ∧ N ≤ # BUF);
postcondition true;
{if BUFLEB ≠ nobuffer ∧ (¬ ROFS → WBUF.offset + WBUF.nbytes + N ≤ LEB_SIZE ∧ N ≤ # BUF)
then if ROFS
then ERR := EROFS
else if WBUF.nbytes + N ≥ PAGESIZE
then let N0 = align↓(WBUF.nbytes + N, PAGESIZE)
in let N1 = N0 - WBUF.nbytes
in let N2 = (WBUF.nbytes + N) % PAGESIZE
in let BUF0 = mkbuf(N0)
in {BUF0 := copy(WBUF.content, 0, BUF0, 0, WBUF.nbytes); BUF0 := copy(BUF, 0, BUF0, WBUF.nbytes, N1);
apersistence_io_write#
(BUFLEB.leb, WBUF.offset, 0, N0, BUF0, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR);
if ERR = ESUCCESS
then {WBUF.content := copy(BUF, N1, WBUF.content, 0, N2); WBUF.offset := WBUF.offset + N0;
WBUF.nbytes := N2}
else ROFS := true}
else {WBUF.content := copy(BUF, 0, WBUF.content, WBUF.nbytes, N); WBUF.nbytes := WBUF.nbytes + N; ERR := ESUCCESS}
else abort
}
read-buf:
wbuf_read_buf#(LNUM, OFFSET, N, BUFLEB, WBUF, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR)
precondition LNUM < # PVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ PVOL[LNUM].mapped?;
postcondition true;
{if LNUM < # PVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ PVOL[LNUM].mapped?
then {apersistence_io_read#(LNUM, OFFSET, 0, N, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR);
if ERR = ESUCCESS ∧ buffered(LNUM) = BUFLEB ∧ OFFSET ≤ WBUF.offset + WBUF.nbytes ∧ WBUF.offset ≤ OFFSET + N
then let BEGINWBUF = (OFFSET ≤ WBUF.offset ⊃ 0;OFFSET - WBUF.offset),
BEGINBUF = (OFFSET ≤ WBUF.offset ⊃ WBUF.offset - OFFSET;0)
in BUF := copy(WBUF.content, BEGINWBUF, BUF, BEGINBUF, min(N - BEGINBUF, WBUF.nbytes - BEGINWBUF))}
else abort
}
get-volume-size:
wbuf_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
precondition true;
postcondition true;
{apersistence_io_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
}
commit:
wbuf_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, ROFS; ERR)
precondition # LPT = # PVOL;
postcondition true;
{if # LPT = # PVOL
then {apersistence_io_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; ERR);
if ERR ≠ ESUCCESS then ROFS := true}
else abort
}
requires-commit:
wbuf_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?)
precondition true;
postcondition true;
{apersistence_io_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?)
}
add-log-leb:
wbuf_add_log_leb#(LNUM, OFFSET, ROFS, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; BUFLEB, WBUF, PLOG; ERR)
precondition ¬ ROFS
→ BUFLEB = buffered(LNUM)
∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data
;
postcondition true;
{if ¬ ROFS
→ BUFLEB = buffered(LNUM)
∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data
then if ROFS
then ERR := EROFS
else {apersistence_io_add_log_leb#(LNUM, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; PLOG; ERR);
if ERR = ESUCCESS then wbuf_move_buf#(LNUM, OFFSET, ROFS, PVOL; BUFLEB, WBUF; ERR)}
else abort
}
remap:
wbuf_remap#(LNUM, BUFLEB, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR)
precondition LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB;
postcondition true;
{if LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB
then apersistence_io_remap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR)
else abort
}
unmap:
wbuf_unmap#(LNUM, BUFLEB, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL)
precondition LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB;
postcondition true;
{if LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB
then apersistence_io_unmap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL)
else abort
}
get-page-size:wbuf_get_page_size#(PAGESIZE; ; N) precondition true; postcondition true;{N := PAGESIZE}
get-leb-size:
wbuf_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
precondition true;
postcondition true;
{apersistence_io_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
}
format:
wbuf_format#
(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; WBUF, PAGESIZE, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, BUFLEB, ROFS; ERR)
precondition VOLSIZE = # LPT ∧ SIZE = LEB_SIZE;
postcondition true;
{if VOLSIZE = # LPT ∧ SIZE = LEB_SIZE
then {apersistence_io_format#(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; ; PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, ERR);
if ERR = ESUCCESS
then {apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; PAGESIZE); BUFLEB := nobuffer;
WBUF.content := mkbuf(PAGESIZE); ROFS := false}}
else abort
}
recover:
wbuf_recover#
(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, WBUF, PAGESIZE, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, BUFLEB, ROFS; ERR)
precondition true;
postcondition true;
{{apersistence_io_recover#(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, PVOL; ERR);
if ERR = ESUCCESS
then {apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; PAGESIZE); BUFLEB := nobuffer;
WBUF.content := mkbuf(PAGESIZE); ROFS := false}}
}
end data asm specification