[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
ubi
using ubi-base,
ubi-crash-recovery-base
,
aubi-io-asm
,
debug
procedures ubi_next_sqnum# : nat : nat ;
ubi_get_volume_size# volid × volumes : : nat ;
ubi_create_volume# volid × nat × nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error nondeterministic;
ubi_read# volid × nat × nat × nat × nat × volumes × nat × apebs : buffer × nat-set : error nondeterministic;
ubi_write# volid × nat × nat × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
nondeterministic;
ubi_write_multiple# volid × nat × nat × nat × nat × buffer × nat-set × nat : volumes × wlarray × queue × nat × apebs : error
nondeterministic;
ubi_write_once# volid × nat × nat × nat × nat × buffer : volumes × wlarray × queue × nat × apebs : error nondeterministic;
ubi_unmap# volid × nat : volumes × wlarray × queue × nat-set nonfunctional ;
ubi_erase# volid × nat × nat × nat : volumes × wlarray × queue × nat-set × apebs : error nondeterministic;
ubi_map# volid × nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error nondeterministic;
ubi_change# volid × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error nondeterministic;
ubi_wear_leveling_worker# nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error nondeterministic;
ubi_wl_put_peb# lebref × nat : wlarray × queue nonfunctional ;
ubi_erase_worker_helper# nat : wlarray × apebs : error nondeterministic;
ubi_erase_worker# : wlarray × queue × apebs nonfunctional nondeterministic;
ubi_erase_all# volumes × nat-set × nat × nat : wlarray × queue × apebs : error nondeterministic;
ubi_wl_get_free_min# wlarray : nat : bool ;
ubi_wl_get_used_min# wlarray : nat : bool ;
ubi_wl_find_free_max_below# nat × wlarray : nat nonfunctional ;
ubi_wl_get_peb# : nat × wlarray × queue × apebs : error nondeterministic;
ubi_get_pebs_for_wl# wlarray : nat × nat × nat-set : bool nondeterministic;
ubi_atomic_leb_change# volid × nat × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
nondeterministic;
ubi_sync_device# volumes × nat-set × nat × nat : wlarray × queue × apebs : error nondeterministic;
ubi_get_page_size# nat : : nat ;
ubi_get_leb_size# nat : : nat ;
ubi_format# : wlarray × nat × nat × apebs × volumes × queue × nat-set × nat : nat × error nondeterministic;
ubi_recover# apebs : volumes × wlarray × queue × nat-set × nat × nat × nat : nat × error nondeterministic;
ubi_init_vols_sizes# recoveryentries × wlarray × apebs : vtbl × volumes nonfunctional nondeterministic;
ubi_init_vols_mappings# nat × apebs : recoveryentries × volumes × wlarray × queue × nat-set nonfunctional nondeterministic;
ubi_scan_all# nat × apebs : recoveryentries × wlarray × queue × nat-set × nat : nat × nat × nat-list × error nondeterministic;
ubi_fix_ecs# nat : nat-list × wlarray nonfunctional ;
variables VOLID : volid flexible;
VOLID0 : volid flexible;
M : nat flexible;
LNUM : nat flexible;
TRIES : nat flexible;
EC : nat flexible;
FROM : nat flexible;
TO : nat flexible;
SQNUM : nat flexible;
VTBLPNUM : nat flexible;
EQENT : erasequeueentry flexible;
VOLS : volumes flexible;
WLARRAY : wlarray flexible;
EBAENT : ebaentry flexible;
EBATBL : ebatbl flexible;
WLUSED : wlentry flexible;
WLFREE : wlentry flexible;
LREF : lebref flexible;
ERASEQ : queue flexible;
TMPERASEQ : queue flexible;
FREEECS : nat-set flexible;
USEDECS : nat-set flexible;
CHKSM : nat flexible;
BFLIPSET : nat-set flexible;
RECS : recoveryentries flexible;
INVALIDECS : nat-list flexible;
VALIDCOUNT : nat flexible;
VALIDECSUM : nat flexible;
LEBSIZE : nat flexible;
PAGESIZE : nat flexible;
VALID : bool flexible;
VTBL : vtbl flexible;
FOUND : bool flexible;
vtblpnum : nat;
sqnum : nat;
BITFLIPS0 : bool flexible;
PNUM0 : nat flexible;
LADR : lebadress flexible;
state variables VOLS : volumes flexible;
WLARRAY : wlarray flexible;
ERASEQ : queue flexible;
BFLIPSET : nat-set flexible;
VTBLPNUM : nat flexible;
SQNUM : nat flexible;
LEBSIZE : nat flexible;
PAGESIZE : nat flexible;
initialization procedure ubi_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ ubi-cons(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM);
lebsize : ⊦ LEBSIZE = LEB_SIZE;
pagesize : ⊦ PAGESIZE = EB_PAGE_SIZE;
recovery procedure ubi_recover#
if ERR = ESUCCESS
declarations next-sqnum : ubi_next_sqnum#(; SQNUM; N){N := SQNUM; SQNUM := SQNUM + 1};
get-volume-size:
ubi_get_volume_size#(VOLID, VOLS; ; N)
precondition VOLID ∈ VOLS;
postcondition true;
{if VOLID ∈ VOLS then N := # VOLS[VOLID] else abort
}
create-volume:
ubi_create_volume#(VOLID, N, LEBSIZE, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ id(APEBS, APEBS`, mapped-pebs(VOLS))
∧ ( ERR = ESUCCESS
→ ¬ VOLID ∈ VOLS` ∧ VOLS = (VOLS`)[VOLID, fill(mkebatbl(N), unmapped)] ∧ ERASEQ.lebrefs ⊆ {VTBL_VOLID × VTBL_LNUM} )
∧ (ERR ≠ ESUCCESS → ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ∧ VOLS = VOLS`)
;
{if VOLID ∈ VOLS ∨ VOLID = VTBL_VOLID
then ERR := EINVAL
else if ENCODED_NAT_SIZE + (# VOLS + 1) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) > LEBSIZE
then ERR := ENOSPC
else let PNUM = ?
in {ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR);
if ERR = ESUCCESS
then {ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR);
if ERR = ESUCCESS
then let VTBL = to-vtbl(VOLS)
in {VTBL[VOLID] := N;
let BUF = mkbuf(LEBSIZE), VTBL = to-vtbl(VOLS)
in {VTBL[VOLID] := N; encode_vtbl#(; VTBL, BUF; ERR);
if ERR = ESUCCESS
then {ubi_atomic_leb_change#
(VTBL_VOLID, VTBL_LNUM, PNUM, LEBSIZE, BUF, PAGESIZE
; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS
; ERR);
if ERR = ESUCCESS
then {VOLS[VOLID] := mkebatbl(N); VOLS[VOLID] := fill(VOLS[VOLID], unmapped)}}}}}}
}
read:
ubi_read#(VOLID, LNUM, OFFSET, N0, N, VOLS, LEBSIZE, APEBS; BUF, BFLIPSET; ERR)
precondition VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEBSIZE ∧ N0 + N ≤ # BUF;
postcondition true;
{if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEBSIZE ∧ N0 + N ≤ # BUF
then let EBAENT = VOLS[VOLID][LNUM]
in if EBAENT = unmapped
then {BUF := fill(BUF, empty, N0, N); ERR := ESUCCESS}
else let PNUM = EBAENT.pnum, BITFLIPS = ?
in {aubi_io_read_data#(PNUM, OFFSET, N0, N, APEBS; BUF; BITFLIPS, ERR);
if ERR = ESUCCESS ∧ BITFLIPS then BFLIPSET := BFLIPSET ++ PNUM}
else abort
}
write:
ubi_write#(VOLID, LNUM, OFFSET, N0, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
precondition VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE)
∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ (VOLS[VOLID][LNUM] ≠ unmapped → APEBS[VOLS[VOLID][LNUM].pnum].fill ≤ OFFSET)
;
postcondition true;
{if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE)
∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ (VOLS[VOLID][LNUM] ≠ unmapped → APEBS[VOLS[VOLID][LNUM].pnum].fill ≤ OFFSET)
then let EBAENT = VOLS[VOLID][LNUM]
in if EBAENT = unmapped
then ubi_write_multiple#(VOLID, LNUM, OFFSET, N0, N, BUF, BFLIPSET, VTBLPNUM; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR)
else if N ≠ 0
then {aubi_io_write_data#(EBAENT.pnum, OFFSET, N0, N, BUF; APEBS; ERR);
if ERR ≠ ESUCCESS
then {debug#("ubi: failed to write to PEB " + EBAENT.pnum.toString);
let BUF0 = mkbuf(OFFSET + N), BITFLIPS = ?
in {aubi_io_read_data#(EBAENT.pnum, 0, 0, OFFSET, APEBS; BUF0; BITFLIPS, ERR);
if ERR = ESUCCESS
then {BUF0 := copy(BUF, N0, BUF0, OFFSET, N);
debug#("ubi: moving data from PEB " + EBAENT.pnum.toString);
ubi_change#
(VOLID, LNUM, OFFSET + N, BUF0, PAGESIZE
; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS
; ERR)}
else debug#("ubi: failed to read data from PEB " + EBAENT.pnum.toString)}}}
else ERR := ESUCCESS
else abort
}
write-multiple
: ubi_write_multiple#(VOLID, LNUM, OFFSET, N0, N, BUF, BFLIPSET, VTBLPNUM; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR)
{ERR := EIO;
let TRIES = 0
in while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_WRITE_RETRIES
do {/* (prepost-write-multiple
: invariant ubi-cons(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM) ∧ ubi-io-inv(APEBS) ∧ VOLID ∈ VOLS
∧ LNUM < # VOLS[VOLID] ∧ (VOLS`)[VOLID][LNUM] = unmapped ∧ id(APEBS, APEBS`, mapped-pebs(VOLS`))
∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ++ (VOLID × LNUM) ∧ N0 + N ≤ # BUF
∧ (N = 0 → ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR ≠ ESUCCESS → VOLS = VOLS`)
∧ ( ERR = ESUCCESS
→ (∃ n.
VOLS = (VOLS`)[VOLID, (VOLS`)[VOLID][LNUM, ⌜n⌝ ]] ∧ (N ≠ 0 → APEBS[n].fill = OFFSET + N)
∧ (N = 0 → APEBS[n].fill = 0)
∧ APEBS[n].data = mkempbuf(OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - N - OFFSET)))
∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE
wfbound UBI_WRITE_RETRIES + 1 - TRIES)
*/;
ubi_write_once#(VOLID, LNUM, OFFSET, N0, N, BUF; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR); TRIES := TRIES +1}
}
;
write-once
: ubi_write_once#(VOLID, LNUM, OFFSET, N0, N, BUF; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR)
{let PNUM = ?
in {ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR);
if ERR = ESUCCESS
then let M = ?
in {ubi_next_sqnum#(; SQNUM; M); aubi_io_write_vidhdr#(PNUM, avidhdr(VOLID, LNUM, M, 0, 0); APEBS; ERR);
if ERR = ESUCCESS
then {if N ≠ 0 then aubi_io_write_data#(PNUM, OFFSET, N0, N, BUF; APEBS; ERR);
if ERR = ESUCCESS
then {VOLS[VOLID][LNUM] := ⌜PNUM⌝ ; WLARRAY[PNUM].status := used}
else ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ);
skip}
else ubi_wl_put_peb#(none, PNUM; WLARRAY, ERASEQ)}}
}
;
unmap:
ubi_unmap#(VOLID, LNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET)
precondition VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID];
postcondition true;
{if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID]
then let EBAENT = VOLS[VOLID][LNUM]
in if EBAENT ≠ unmapped
then let PNUM = EBAENT.pnum
in {VOLS[VOLID][LNUM] := unmapped; BFLIPSET := BFLIPSET -- PNUM;
ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ)}
else abort
}
erase:
ubi_erase#(VOLID, LNUM, VTBLPNUM, SQNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET, APEBS; ERR)
precondition VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID];
postcondition true;
{if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID]
then {ubi_unmap#(VOLID, LNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET);
ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)}
else abort
}
map:
ubi_map#(VOLID, LNUM, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
precondition VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ VOLS[VOLID][LNUM] = unmapped;
postcondition true;
{if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ VOLS[VOLID][LNUM] = unmapped
then let BUF = mkbuf(0)
in ubi_write#(VOLID, LNUM, 0, 0, 0, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
else abort
}
change:
ubi_change#(VOLID, LNUM, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
precondition N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ is-aligned(N, EB_PAGE_SIZE);
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ (ERR ≠ ESUCCESS → VOLS = VOLS` ∧ id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs)
∧ ( ERR = ESUCCESS
→ VOLID ∈ VOLS` ∧ LNUM < # (VOLS`)[VOLID] ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ++ (VOLID × LNUM)
∧ ((VOLS`)[VOLID][LNUM] ≠ unmapped → id(APEBS, APEBS`, mapped-pebs(VOLS`) -- (VOLS`)[VOLID][LNUM].pnum))
∧ ((VOLS`)[VOLID][LNUM] = unmapped → id(APEBS, APEBS`, mapped-pebs(VOLS`)))
∧ (∃ n.
VOLS = (VOLS`)[VOLID, (VOLS`)[VOLID][LNUM, ⌜n⌝ ]]
∧ APEBS[n].data = subarray(BUF, 0, N) + mkempbuf(LEB_SIZE - N)
∧ APEBS[n].fill = align↑(datasize(BUF, N), EB_PAGE_SIZE)))
;
{if N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ is-aligned(N, EB_PAGE_SIZE)
then let TO = ?
in {ubi_wl_get_peb#(; TO, WLARRAY, ERASEQ, APEBS; ERR);
if ERR = ESUCCESS
then ubi_atomic_leb_change#
(VOLID, LNUM, TO, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR);
if ERR ≠ ESUCCESS then debug#("ubi: change to PEB " + TO.toString + " failed")}
else abort
}
wl-worker:
ubi_wear_leveling_worker#(LEBSIZE, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
precondition true;
postcondition VOLS` = VOLS ∧ id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ++ (VTBL_VOLID × VTBL_LNUM)
∨ (∃ v, m, n.
v ∈ VOLS` ∧ m < # (VOLS`)[v] ∧ (VOLS`)[v][m] ≠ unmapped ∧ VOLS = (VOLS`)[v, (VOLS`)[v][m, ⌜n⌝ ]]
∧ id(APEBS, APEBS`, mapped-pebs(VOLS`) -- (VOLS`)[v][m].pnum) ∧ APEBS[n].data = (APEBS`)[(VOLS`)[v][m].pnum].data
∧ APEBS[n].fill ≤ (APEBS`)[(VOLS`)[v][m].pnum].fill ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ++ (v × m))
;
{let VALID = ?, TO = ?, FROM = ?
in {ubi_get_pebs_for_wl#(WLARRAY; TO, FROM, BFLIPSET; VALID);
if VALID
then let AVHDR = ?, BITFLIPS = ?
in {aubi_io_read_vidhdr#(FROM, APEBS; AVHDR; BITFLIPS, ERR);
if ERR = ESUCCESS
then let BUF = mkbuf(LEBSIZE)
in {aubi_io_read_data#(FROM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS, ERR);
if ERR = ESUCCESS
then ubi_atomic_leb_change#
(AVHDR.vol, AVHDR.leb, TO, LEBSIZE, BUF, PAGESIZE
; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS
; ERR);
if ERR ≠ ESUCCESS
then debug#("ubi: wear-leveling of PEB " + FROM.toString + " to PEB " + TO.toString + " failed");
if ERR = ESUCCESS
then {ubi_erase_worker_helper#(FROM; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.butlast}}}
else ERR := ENOSPC}
}
wl-put-peb
: ubi_wl_put_peb#(LREF, PNUM; WLARRAY, ERASEQ){WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, LREF)}
;
erase-worker-helper
: ubi_erase_worker_helper#(PNUM; WLARRAY, APEBS; ERR)
{ERR := EIO;
let TRIES = 0
in {while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_ERASE_RETRIES
do {WLARRAY[PNUM].ec := WLARRAY[PNUM].ec + 1; aubi_io_sync_erase#(PNUM; APEBS; ERR);
if ERR = ESUCCESS
then aubi_io_write_echdr#(PNUM, aechdr(WLARRAY[PNUM].ec); APEBS; ERR)
else debug#("ubi: erase of PEB " + PNUM.toString + " failed");
TRIES := TRIES + 1};
if ERR = ESUCCESS
then WLARRAY[PNUM].status := free
else {aubi_io_markbad#(PNUM; APEBS; ERR);
if ERR = ESUCCESS
then WLARRAY[PNUM].status := erroneous
else debug#("ubi: marking PEB " + PNUM.toString + " as bad failed")}}
}
;
erase-worker:
ubi_erase_worker#(; WLARRAY, ERASEQ, APEBS)
precondition true;
postcondition true;
{if ERASEQ ≠ []
then let EQENT = ERASEQ.head, ERR = ?
in {ubi_erase_worker_helper#(EQENT.pnum; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.tail}
}
erase-all:
ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)
precondition true;
postcondition id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ ⊆ ERASEQ` ∧ (ERR = ESUCCESS → ERASEQ = []) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ );
{{ERR := ESUCCESS;
while ERR = ESUCCESS ∧ ERASEQ ≠ []
do {/* (inv-erase-all
: invariant ubi-cons(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM) ∧ ubi-io-inv(APEBS)
∧ id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ ⊆ ERASEQ` ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
wfbound (ERR = ESUCCESS ⊃ # ERASEQ;0))
*/;
ubi_erase_worker_helper#(ERASEQ.head.pnum; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.tail}}
}
get-free-min
: ubi_wl_get_free_min#(WLARRAY; N; FOUND)
{FOUND := false;
let M = 0
in while M < # WLARRAY
do {/* (prepost-wl-get-free-min
: invariant M ≤ # WLARRAY ∧ (FOUND → N = free-ecs(WLARRAY, M).min) ∧ (¬ FOUND ↔ free-ecs(WLARRAY, M) = ∅)
wfbound # WLARRAY - M)
*/;
if WLARRAY[M].status = free ∧ (¬ FOUND ∨ WLARRAY[M].ec < N) then {FOUND := true; N := WLARRAY[M].ec}; M := M + 1}
}
;
get-used-min
: ubi_wl_get_used_min#(WLARRAY; PNUM; FOUND)
{FOUND := false;
let M = 0
in while M < # WLARRAY
do {/* (prepost-wl-get-used-min
: invariant M ≤ # WLARRAY
∧ (FOUND → PNUM < M ∧ WLARRAY[PNUM].status = used ∧ WLARRAY[PNUM].ec = used-ecs(WLARRAY, M).min)
∧ (¬ FOUND ↔ used-ecs(WLARRAY, M) = ∅)
wfbound # WLARRAY - M)
*/;
if WLARRAY[M].status = used ∧ (¬ FOUND ∨ WLARRAY[M].ec < WLARRAY[PNUM].ec) then {FOUND := true; PNUM := M}; M := M + 1}
}
;
find-max-below
: ubi_wl_find_free_max_below#(N, WLARRAY; PNUM)
{let FOUND = false, M = 0
in while M < # WLARRAY
do {/* (prepost-wl-free-max-below
: invariant M ≤ # WLARRAY
∧ ( FOUND
→ PNUM < # WLARRAY ∧ WLARRAY[PNUM].status = free
∧ WLARRAY[PNUM].ec = below(free-ecs(WLARRAY, M), N).max)
∧ (¬ FOUND ↔ below(free-ecs(WLARRAY, M), N) = ∅)
wfbound # WLARRAY - M)
*/;
if WLARRAY[M].status = free ∧ WLARRAY[M].ec < N ∧ (¬ FOUND ∨ WLARRAY[M].ec > WLARRAY[PNUM].ec)
then {FOUND := true; PNUM := M};
M := M + 1}
}
;
wl-get-peb
: ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR)
{let FOUND = ?, N = ?
in {ubi_wl_get_free_min#(WLARRAY; N; FOUND);
if ¬ FOUND
then if ERASEQ ≠ []
then {PNUM := ERASEQ.head.pnum; ubi_erase_worker_helper#(PNUM; WLARRAY, APEBS; ERR);
if ERR = ESUCCESS then {ERASEQ := ERASEQ.tail; if WLARRAY[PNUM].status ≠ free then ERR := ENOSPC} else ERR := ENOSPC}
else ERR := ENOSPC
else {ubi_wl_find_free_max_below#(N + WL_THRESHOLD, WLARRAY; PNUM); ERR := ESUCCESS}}
}
;
get-pebs-for-wl
: ubi_get_pebs_for_wl#(WLARRAY; TO, FROM, BFLIPSET; VALID)
{VALID := false;
let FOUND = ?, N = ?
in {ubi_wl_get_free_min#(WLARRAY; N; FOUND);
if FOUND
then {ubi_wl_find_free_max_below#(N + 2 * WL_THRESHOLD, WLARRAY; TO);
if BFLIPSET ≠ ∅
then choose N with N ∈ BFLIPSET in {FROM := N; BFLIPSET := BFLIPSET -- N; VALID := true}
else {ubi_wl_get_used_min#(WLARRAY; FROM; FOUND);
if FOUND ∧ WLARRAY[TO].ec ≥ WLARRAY[FROM].ec + WL_THRESHOLD then VALID := true}}}
}
;
atomic-leb-change
: ubi_atomic_leb_change#(VOLID, LNUM, TO, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)
{ERR := ESUCCESS; N := datasize(BUF, N);
let M = ?
in {ubi_next_sqnum#(; SQNUM; M);
let AVHDR = avidhdr(VOLID, LNUM, M, N, 0)
in {if N ≠ 0 then AVHDR.checksum := checksum(BUF, N); aubi_io_write_vidhdr#(TO, AVHDR; APEBS; ERR);
if ERR = ESUCCESS then if N > 0 then aubi_io_write_data_wl#(TO, align↑(N, PAGESIZE), BUF; APEBS; ERR);
if ERR = ESUCCESS
then {if VOLID = VTBL_VOLID ∧ LNUM = VTBL_LNUM
then {ubi_wl_put_peb#(VTBL_VOLID × VTBL_LNUM, VTBLPNUM; WLARRAY, ERASEQ); BFLIPSET := BFLIPSET -- VTBLPNUM;
VTBLPNUM := TO}
else {if VOLS[VOLID][LNUM] ≠ unmapped
then let PNUM = VOLS[VOLID][LNUM].pnum
in {ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ); BFLIPSET := BFLIPSET -- PNUM};
VOLS[VOLID][LNUM] := ⌜TO⌝ };
WLARRAY[TO].status := used}
else ubi_wl_put_peb#(none, TO; WLARRAY, ERASEQ)}}
}
;
sync-device:
ubi_sync_device#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)
precondition true;
postcondition id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ ⊆ ERASEQ` ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ );
{ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)
}
get-page-size:ubi_get_page_size#(PAGESIZE; ; N) precondition true; postcondition true;{N := PAGESIZE}
get-leb-size:ubi_get_leb_size#(LEBSIZE; ; N) precondition true; postcondition true;{N := LEBSIZE}
format:
ubi_format#(; WLARRAY, VTBLPNUM, LEBSIZE, APEBS, VOLS, ERASEQ, BFLIPSET, SQNUM; PAGESIZE, ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → VOLS = ∅);
{{aubi_io_format#(; ; APEBS, ERR); aubi_io_get_leb_size#(APEBS; ; LEBSIZE); aubi_io_get_page_size#(APEBS; ; PAGESIZE);
if ERR ≠ ESUCCESS
then debug#("ubi: ubi-io format failed")
else let N = ?, PNUM = 0
in {aubi_io_get_blockcount#(APEBS; ; N); WLARRAY := mkwlarray(N); VTBLPNUM := N; ERR := ESUCCESS;
while PNUM < N ∧ ERR = ESUCCESS
do {/* (inv-format
: invariant PNUM ≤ # APEBS ∧ N = # APEBS ∧ # WLARRAY = # APEBS ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ ubi-io-initial(APEBS) ∧ VTBLPNUM ≤ # APEBS
∧ (∀ n3.
n3 < PNUM
→ (APEBS[n3].bad → WLARRAY[n3] = wl-entry(0, erroneous))
∧ ( ¬ APEBS[n3].bad
→ APEBS[n3].echdr.valid? ∧ WLARRAY[n3] = wl-entry(APEBS[n3].echdr.ec, free)
∧ APEBS[n3].vidhdr = empty))
∧ (VTBLPNUM ≠ # APEBS → ¬ APEBS[VTBLPNUM].bad))
wfbound N - PNUM)
*/;
let ISBAD = ?
in {aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR);
if ERR = ESUCCESS
then if ¬ ISBAD
then let AEHDR = ?, BITFLIPS = ?
in {aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR);
if ERR = ESUCCESS ∧ VTBLPNUM = N then VTBLPNUM := PNUM;
if ERR = ESUCCESS ∧ AEHDR.valid? then WLARRAY[PNUM] := wl-entry(AEHDR.ec, free)}
else WLARRAY[PNUM] := wl-entry(0, erroneous);
PNUM := PNUM + 1}};
if ERR = ESUCCESS
then if VTBLPNUM = N
then ERR := ENOSPC
else {aubi_io_write_vidhdr#(VTBLPNUM, avidhdr(VTBL_VOLID, VTBL_LNUM, 0, 0, 0); APEBS; ERR);
if ERR = ESUCCESS
then if ENCODED_NAT_SIZE > LEBSIZE
then ERR := ENOSPC
else let BUF = mkbuf(LEBSIZE), VTBL = ∅
in {encode_vtbl#(; VTBL, BUF; ERR);
if ERR = ESUCCESS then aubi_io_write_data#(VTBLPNUM, 0, 0, LEBSIZE, BUF; APEBS; ERR)};
VOLS := ∅; WLARRAY[VTBLPNUM].status := used; ERASEQ := []; SQNUM := 1; BFLIPSET := ∅}}}
}
recover:
ubi_recover#(APEBS; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, LEBSIZE; PAGESIZE, ERR)
precondition true;
postcondition (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ ( ERR = ESUCCESS
→ is-max(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM) ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs
∧ VOLS` ⊆ VOLS ∧ VOLS⌈VOLS`, ERASEQ`⌉)
;
{{aubi_io_recovery#(APEBS); VOLS := ∅; aubi_io_get_leb_size#(APEBS; ; LEBSIZE); aubi_io_get_page_size#(APEBS; ; PAGESIZE);
let RECS = ∅, INVALIDECS = [], VALIDCOUNT = 0, VALIDECSUM = 0
in {ubi_scan_all#(LEBSIZE, APEBS; RECS, WLARRAY, ERASEQ, BFLIPSET, SQNUM; VALIDCOUNT, VALIDECSUM, INVALIDECS, ERR);
if ¬ VTBL_VOLID × VTBL_LNUM ∈ RECS then ERR := EINVAL;
if ERR = ESUCCESS
then let BUF = mkbuf(LEBSIZE), BITFLIPS = ?
in {VTBLPNUM := RECS[VTBL_VOLID × VTBL_LNUM].pnum;
aubi_io_read_data#(VTBLPNUM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS, ERR);
if BITFLIPS then BFLIPSET := BFLIPSET ++ VTBLPNUM;
if ERR = ESUCCESS
then let VTBL = ?
in {decode_vtbl#(BUF; ; VTBL, ERR);
if ERR = ESUCCESS
then {ubi_init_vols_sizes#(RECS, WLARRAY, APEBS; VTBL, VOLS);
ubi_init_vols_mappings#(VTBLPNUM, APEBS; RECS, VOLS, WLARRAY, ERASEQ, BFLIPSET);
let N = (VALIDCOUNT = 0 ⊃ 0;VALIDECSUM / VALIDCOUNT) in ubi_fix_ecs#(N; INVALIDECS, WLARRAY)}}}}}
}
init-vols-sizes
: ubi_init_vols_sizes#(RECS, WLARRAY, APEBS; VTBL, VOLS)
{VOLS := ∅;
while VTBL ≠ ∅
do {/* (prepost-init-vols-sizes
: invariant to-vtbl(VOLS) ⊥ VTBL ∧ is-encoded(to-vtbl(VOLS) ∪ VTBL, APEBS[RECS[VTBL_VOLID × VTBL_LNUM].pnum].data)
∧ valid-vtbl-weak(APEBS, RECS[VTBL_VOLID × VTBL_LNUM].pnum) ∧ valid-recs(APEBS, WLARRAY, RECS)
∧ RECS[VTBL_VOLID × VTBL_LNUM].pnum < # APEBS ∧ VTBL_VOLID × VTBL_LNUM ∈ RECS ∧ unmapped-vols(VOLS)
∧ # APEBS = # WLARRAY
wfbound # VTBL)
*/;
choose VOLID
with VOLID ∈ VTBL
in {VOLS[VOLID] := mkebatbl(VTBL[VOLID]); VOLS[VOLID] := fill(VOLS[VOLID], unmapped); VTBL := VTBL -- VOLID}}
}
;
init-vols
: ubi_init_vols_mappings#(VTBLPNUM, APEBS; RECS, VOLS, WLARRAY, ERASEQ, BFLIPSET)
{RECS := RECS -- (VTBL_VOLID × VTBL_LNUM);
while RECS ≠ ∅
do {/* (prepost-init-vols-mappings
: invariant unique-sqns(APEBS) ∧ valid-vtbl(APEBS, VOLS, WLARRAY, VTBLPNUM) ∧ ¬ VTBL_VOLID ∈ VOLS
∧ ¬ VTBL_VOLID × VTBL_LNUM ∈ RECS ∧ # APEBS = # WLARRAY ∧ valid-wl(APEBS, WLARRAY)
∧ valid-eraseq(WLARRAY, ERASEQ)
∧ (∃ vtbl. is-encoded(vtbl, APEBS[VTBLPNUM].data) ∧ valid-eraseq-strong(APEBS, vtbl, ERASEQ))
∧ bflipset-cons(BFLIPSET, WLARRAY) ∧ RECS ⊥ VOLS ∧ ERASEQ` ⊆ ERASEQ
∧ (∀ v, m, n.
v × m ∈ RECS ∧ RECS[v × m].pnum = n ∨ v ∈ VOLS ∧ m < # VOLS[v] ∧ VOLS[v][m] = ⌜n⌝
↔ WLARRAY[n].status = used ∧ n < # APEBS ∧ APEBS[n].vidhdr.valid? ∧ APEBS[n].vidhdr.vol = v
∧ APEBS[n].vidhdr.leb = m ∧ n ≠ VTBLPNUM)
wfbound # RECS)
*/;
choose LADR
with LADR ∈ RECS
in let N = RECS[LADR].pnum
in {if LADR.vol ∈ VOLS ∧ LADR.leb < # VOLS[LADR.vol]
then VOLS[LADR.vol][LADR.leb] := ⌜N⌝
else {WLARRAY[N].status := erasing; ERASEQ := ERASEQ + eq-entry(N, LADR.vol × LADR.leb); BFLIPSET := BFLIPSET -- N};
RECS := RECS -- LADR}}
}
;
scan-all
: ubi_scan_all#(LEBSIZE, APEBS; RECS, WLARRAY, ERASEQ, BFLIPSET, SQNUM; VALIDCOUNT, VALIDECSUM, INVALIDECS, ERR)
{RECS := ∅; BFLIPSET := ∅; VALIDCOUNT := 0; VALIDECSUM := 0; INVALIDECS := [];
let N = ?, PNUM = 0
in {ERASEQ := []; SQNUM := 0; ERR := ESUCCESS; aubi_io_get_blockcount#(APEBS; ; N); WLARRAY := mkwlarray(N);
WLARRAY := fill(WLARRAY, wl-entry(0, free));
while PNUM < N ∧ ERR = ESUCCESS
do {/* (prepost-scan-all
: invariant scan-all-inv(PNUM, APEBS, RECS, WLARRAY, ERASEQ, BFLIPSET, INVALIDECS, SQNUM, ERR)
wfbound # APEBS - PNUM)
*/;
let ISBAD = ?
in {aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR);
if ERR = ESUCCESS
then if ISBAD
then WLARRAY[PNUM].status := erroneous
else let AEHDR = ?, BITFLIPS = ?
in {aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR);
if ERR = ESUCCESS
then if ¬ AEHDR.valid?
then {INVALIDECS := PNUM + INVALIDECS; WLARRAY[PNUM].status := erasing;
ERASEQ := ERASEQ + eq-entry(PNUM, none)}
else let AVHDR = ?
in {VALIDCOUNT := VALIDCOUNT + 1; VALIDECSUM := VALIDECSUM + AEHDR.ec;
WLARRAY[PNUM].ec := AEHDR.ec; aubi_io_read_vidhdr#(PNUM, APEBS; AVHDR; BITFLIPS, ERR);
if ERR = ESUCCESS
then if AVHDR = empty
then if BITFLIPS
then {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)}
else WLARRAY[PNUM].status := free
else if AVHDR.valid?
then let BUF = mkbuf(LEBSIZE)
in {if AVHDR.size ≠ 0
then let BITFLIPS0 = ?
in {aubi_io_read_data#
(PNUM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS0, ERR);
BITFLIPS := BITFLIPS ∨ BITFLIPS0};
if ERR = ESUCCESS
then let LADR = AVHDR.vol × AVHDR.leb, N = 0
in {if LADR ∈ RECS then N := RECS[LADR].sqn;
if AVHDR.size ≠ 0
→ AVHDR.size ≤ datasize(BUF)
∧ AVHDR.checksum = checksum(BUF, AVHDR.size)
then {SQNUM := max(SQNUM, AVHDR.sqn + 1);
if AVHDR.sqn ≥ N
then {WLARRAY[PNUM].status := used;
if BITFLIPS then BFLIPSET := BFLIPSET ++ PNUM;
if LADR ∈ RECS
then let PNUM0 = RECS[LADR].pnum
in {BFLIPSET := BFLIPSET -- PNUM0;
WLARRAY[PNUM0].status := erasing;
ERASEQ
:= ERASEQ
+ eq-entry
(PNUM0, AVHDR.vol × AVHDR.leb)};
RECS[LADR] := recovery-entry(PNUM, AVHDR.sqn)}
else {WLARRAY[PNUM].status := erasing;
ERASEQ
:= ERASEQ + eq-entry(PNUM, LADR.vol × LADR.leb)}}
else {WLARRAY[PNUM].status := erasing;
ERASEQ := ERASEQ + eq-entry(PNUM, none)}}}
else {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)}}};
PNUM := PNUM + 1}}}
}
;
fix-ecs
: ubi_fix_ecs#(N; INVALIDECS, WLARRAY)
{while INVALIDECS ≠ []
do {/* (prepost-fix-ecs
: invariant ∃ nx.
INVALIDECS` = nx + INVALIDECS ∧ WLARRAY = (WLARRAY`).mapIndices(nx, λ wle. wle.ec:= N)
∧ valid-indices(WLARRAY, nx) ∧ ¬ dups(INVALIDECS`)
wfbound # INVALIDECS)
*/;
WLARRAY[INVALIDECS.head].ec := N; INVALIDECS := INVALIDECS.tail}
}
;
end data asm specification