[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_io
using mtd-asm
,
ubi-io-base
constants UBI_READ_RETRIES : nat;
procedures ubi_io_read# nat × nat × nat × nat × pebs : buffer : bool × error nondeterministic;
ubi_io_read_echdr# nat × nat × pebs : aecheader : bool × error nondeterministic;
ubi_io_write_echdr# nat × aecheader × nat : pebs : error nondeterministic;
ubi_io_read_vidhdr# nat × nat × pebs : avidheader : bool × error nondeterministic;
ubi_io_write_vidhdr# nat × avidheader × nat : pebs : error nondeterministic;
ubi_io_read_data# nat × nat × nat × nat × nat × pebs : buffer : bool × error nondeterministic;
ubi_io_write_data# nat × nat × nat × nat × buffer × nat : pebs : error nondeterministic;
ubi_io_write_data_wl# nat × nat × buffer × nat : pebs : error nondeterministic;
ubi_io_sync_erase# nat : pebs : error nondeterministic;
ubi_io_markbad# nat : pebs : error nondeterministic;
ubi_io_isbad# nat × pebs : : bool × error nondeterministic;
ubi_io_get_blockcount# pebs : : nat ;
ubi_io_get_page_size# nat : : nat ;
ubi_io_get_leb_size# nat × pebs : : nat ;
ubi_io_recovery# pebs : : nat ;
ubi_io_format# : nat × pebs : error nondeterministic;
variables EHDR : echeader flexible;
VHDR : vidheader flexible;
TRIES : nat flexible;
AEHDR : aecheader flexible;
AVHDR : avidheader flexible;
M : nat flexible;
PAGESIZE : nat flexible;
state variables PAGESIZE : nat flexible;
initialization procedure ubi_io_format#
if ERR = ESUCCESS
sequential
invariants page-size : ⊦ PAGESIZE = EB_PAGE_SIZE;
recovery procedure ubi_io_recovery#
declarations io-read:
ubi_io_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF;
postcondition # BUF = # BUF` ∧ range=(BUF, 0, BUF`, 0, N0) ∧ range=(BUF, N0 + N, BUF`, N0 + N, # BUF` - N0 + N)
∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → subarray(BUF, N0, N) = subarray(PEBS[PNUM].data, OFFSET, N))
;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF
then {ERR := EIO; BITFLIPS := false;
let TRIES = 0
in while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_READ_RETRIES
do {/* (inv-io-read
: invariant PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF
∧ TRIES ≤ UBI_READ_RETRIES + 1 ∧ # BUF = # BUF` ∧ range=(BUF, 0, BUF`, 0, N0)
∧ range=(BUF, N0 + N, BUF`, N0 + N, # BUF` - N0 + N) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ (ERR = ESUCCESS → subarray(BUF, N0, N) = subarray(PEBS[PNUM].data, OFFSET, N))
wfbound UBI_READ_RETRIES + 1 - TRIES)
*/;
mtd_asm_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR);
if ERR ≠ ESUCCESS then debug#("ubi-io: failed to read from PEB " + PNUM.toString); TRIES := TRIES +1}}
else abort
}
read-echdr:
ubi_io_read_echdr#(PNUM, PAGESIZE, PEBS; AEHDR; BITFLIPS, ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad
then let BUF = mkbuf(PAGESIZE)
in {ubi_io_read#(PNUM, 0, 0, PAGESIZE, PEBS; BUF; BITFLIPS, ERR);
if ERR = ESUCCESS
then if isempty(BUF)
then AEHDR := empty
else let EHDR = ? in {decode_echeader#(PAGESIZE, BUF; EHDR; ERR); if ERR = ESUCCESS then AEHDR := aechdr(EHDR.ec)}}
else abort
}
write-echdr:
ubi_io_write_echdr#(PNUM, AEHDR, PAGESIZE; PEBS; ERR)
precondition PNUM < # PEBS ∧ AEHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 0;
postcondition true;
{if PNUM < # PEBS ∧ AEHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 0
then let BUF = mkbuf(PAGESIZE), EHDR = echdr(AEHDR.ec)
in {encode_echeader#(PAGESIZE, EHDR; BUF; ERR);
if ERR = ESUCCESS then mtd_asm_write#(PNUM, 0, 0, PAGESIZE, BUF; PEBS; ERR)}
else abort
}
read-vidhdr:
ubi_io_read_vidhdr#(PNUM, PAGESIZE, PEBS; AVHDR; BITFLIPS, ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad
then let BUF = mkbuf(PAGESIZE)
in {ubi_io_read#(PNUM, PAGESIZE, 0, PAGESIZE, PEBS; BUF; BITFLIPS, ERR);
if ERR = ESUCCESS
then if isempty(BUF)
then AVHDR := empty
else let VHDR = ?
in {decode_vidheader#(PAGESIZE, BUF; VHDR; ERR);
if ERR = ESUCCESS then AVHDR := avidhdr(VHDR.vol, VHDR.leb, VHDR.sqn, VHDR.size, VHDR.checksum)}}
else abort
}
write-vidhdr:
ubi_io_write_vidhdr#(PNUM, AVHDR, PAGESIZE; PEBS; ERR)
precondition PNUM < # PEBS ∧ AVHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = EB_PAGE_SIZE;
postcondition true;
{if PNUM < # PEBS ∧ AVHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = EB_PAGE_SIZE
then let BUF = mkbuf(PAGESIZE), VHDR = vidhdr(AVHDR.vol, AVHDR.leb, AVHDR.sqn, AVHDR.size, AVHDR.checksum)
in {encode_vidheader#(PAGESIZE, VHDR; BUF; ERR);
if ERR = ESUCCESS then mtd_asm_write#(PNUM, PAGESIZE, 0, PAGESIZE, BUF; PEBS; ERR)}
else abort
}
read-data:
ubi_io_read_data#(PNUM, OFFSET, N0, N, PAGESIZE, PEBS; BUF; BITFLIPS, ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
then ubi_io_read#(PNUM, OFFSET + 2 * PAGESIZE, N0, N, PEBS; BUF; BITFLIPS, ERR)
else abort
}
write-data:
ubi_io_write_data#(PNUM, OFFSET, N0, N, BUF, PAGESIZE; PEBS; ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET + 2 * EB_PAGE_SIZE ∧ OFFSET + N ≤ LEB_SIZE
∧ N0 + N ≤ # BUF ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET + 2 * EB_PAGE_SIZE ∧ OFFSET + N ≤ LEB_SIZE
∧ N0 + N ≤ # BUF ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
then mtd_asm_write#(PNUM, OFFSET + 2 * PAGESIZE, N0, N, BUF; PEBS; ERR)
else abort
}
write-data-wl:
ubi_io_write_data_wl#(PNUM, N, BUF, PAGESIZE; PEBS; ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 2 * EB_PAGE_SIZE ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF
∧ is-aligned(N, EB_PAGE_SIZE)
;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 2 * EB_PAGE_SIZE ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF
∧ is-aligned(N, EB_PAGE_SIZE)
then mtd_asm_write#(PNUM, 2 * PAGESIZE, 0, N, BUF; PEBS; ERR)
else abort
}
sync-erase:
ubi_io_sync_erase#(PNUM; PEBS; ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then mtd_asm_erase#(PNUM; PEBS; ERR) else abort
}
markbad:
ubi_io_markbad#(PNUM; PEBS; ERR)
precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
postcondition true;
{if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then mtd_asm_markbad#(PNUM; PEBS; ERR) else abort
}
isbad:
ubi_io_isbad#(PNUM, PEBS; ; ISBAD, ERR)
precondition PNUM < # PEBS;
postcondition true;
{if PNUM < # PEBS then mtd_asm_isbad#(PNUM, PEBS; ; ISBAD, ERR) else abort
}
get-blockcount:ubi_io_get_blockcount#(PEBS; ; N) precondition true; postcondition true;{mtd_asm_get_blockcount#(PEBS; ; N)}
get-page-size:ubi_io_get_page_size#(PAGESIZE; ; N) precondition true; postcondition true;{N := PAGESIZE}
get-leb-size:
ubi_io_get_leb_size#(PAGESIZE, PEBS; ; N)
precondition true;
postcondition true;
{{mtd_asm_get_peb_size#(PEBS; ; N); N := N - 2 * PAGESIZE}
}
recovery:ubi_io_recovery#(PEBS; ; PAGESIZE) precondition true; postcondition true;{mtd_asm_get_page_size#(PEBS; ; PAGESIZE)}
format:
ubi_io_format#(; PAGESIZE, PEBS; ERR)
precondition true;
postcondition (ERR = ESUCCESS → ubi-io-initial(PEBS)) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ );
{{mtd_asm_init#(; ; PEBS, ERR); mtd_asm_get_page_size#(PEBS; ; PAGESIZE);
if ERR = ESUCCESS
then let N = ?
in {mtd_asm_get_blockcount#(PEBS; ; N);
let M = 0
in while M < N ∧ ERR = ESUCCESS
do {/* (inv-format
: invariant M ≤ N ∧ N = # PEBS ∧ mtd-cons(PEBS) ∧ (ERR = ESUCCESS → ubi-io-initial(subarray(PEBS, 0, M)))
∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ )
wfbound N - M)
*/;
let ISBAD = ?
in {mtd_asm_isbad#(M, PEBS; ; ISBAD, ERR);
if ERR = ESUCCESS ∧ ¬ ISBAD
then let AEHDR = ?, BITFLIPS = ?
in {ubi_io_read_echdr#(M, PAGESIZE, PEBS; AEHDR; BITFLIPS, ERR);
let N = (ERR = ESUCCESS ∧ AEHDR.valid? ⊃ AEHDR.ec + 1;0)
in {mtd_asm_erase#(M; PEBS; ERR);
if ERR = ESUCCESS then ubi_io_write_echdr#(M, aechdr(N), PAGESIZE; PEBS; ERR)}}};
M := M + 1}}}
}
end data asm specification