[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. 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,

Theorem gc-copy

gjournal_gc_copy#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED; ERR) {if NDLIST.keys.toSet ⊆ dom PRI ∧ ¬ dups(NDLIST.keys) ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ key-cons(NDLIST) then {ERR := ESUCCESS; while ERR = ESUCCESS ∧ NDLIST ≠ [] do {/* (inv-gc-copy : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (∃ ndx0. NDLIST` = ndx0 + NDLIST) ∧ JMAXINO ≥ JMAXINO` ∧ (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) ∧ PRI.inos < JMAXINO ∧ PRI.lebs ⊆ dom PSTORE ∧ refsize-cons(PSTORE, range PRI) ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL) ∧ ri-inj(PRI) ∧ NDLIST.keys.toSet ⊆ dom PRI ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ dom PSTORE` ⊆ dom PSTORE ∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅ ∧ (∃ ax, ndx0, ndx1. NDLIST` = ndx0 + ndx1 ∧ (ERR = ESUCCESS → ndx1 = NDLIST) ∧ new(ax, nodes(PSTORE` ↓, PINVAL`)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ PRI = (PRI`)[ndx0.keys, ax] ∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)[ax, ndx0] ∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) + ax) wfbound (ERR = ESUCCESS ⊃ # NDLIST;0)) */; let SIZE = 0, EMPTY? = ? in {index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?); if ¬ EMPTY? then {index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; SIZE); if SIZE < NDLIST.head.flashsize then SIZE := 0}; let NDLIST0 = [], ADRLIST = [], N = ? in {index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); gjournal_split_nodes#(N - SIZE; NDLIST, NDLIST0); if NDLIST0 = [] then ERR := EINVAL else {gjournal_journal_addn# (NDLIST0, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then gjournal_gc_update_index# (JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, NDLIST0, JMAXINO, PRI, PSTORE)}}}}} else abort }