[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

gjournal_journal_gc#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED) {if ri-cons(PRI, nodes(PSTORE ↓, PINVAL)) then let LNUM = ?, ERR = ? in {index_get_gc_block#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LNUM; ERR); if ERR = ESUCCESS then let N = ? in {debug#("gjournal: garbage collecting LEB " + LNUM.toString); index_get_gblock_refsize#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); if N ≠ 0 then let ADRLIST = [], GNDLIST = [], NDLIST = [] in {index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; ERR); if ERR ≠ ESUCCESS then debug#("gjournal: failed to read LEB " + LNUM.toString + " during GC") else gjournal_gc_referenced_nodes# (LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; NDLIST, ERR); if ERR = ESUCCESS then {gjournal_gc_copy# (DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + LNUM.toString + " to journal head during GC")}}}; if ERR = ESUCCESS then index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR); if ERR = ESUCCESS then index_deallocate_gnd#(LNUM, PRI, PFI, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE; ERR)} else abort }