data asm specification 
   pcache

   using error-class
, 
         nat-div
, 
         pcache-del-ops
, 
         cache-base

   

   
   
   
   
   procedures pcache_format#  :  : pcache × error  ;
              pcache_recovery#  :  : pcache × error  ;
              pcache_get# nat × nat × pcache : bool × buffer × error nonfunctional ;
              pcache_set# nat × nat × buffer × bool : error × pcache nonfunctional ;
              pcache_check_page# nat × nat × pcache : bool × bool × error nonfunctional ;
              pcache_set_status# nat × nat × bool : error × pcache nonfunctional nondeterministic;
              pcache_delete# nat × nat : error × pcache nonfunctional ;
              pcache_evict# nat : error × pcache nonfunctional ;
              pcache_truncate# nat × nat × nat : error × pcache nonfunctional ;
   variables  PCACHE : pcache flexible;
              INO : nat flexible;
              N : nat flexible;
              SIZE : nat flexible;
              PAGENO : nat flexible;
              HIT : bool flexible;
              DIRTY : bool flexible;
              BUF : buffer flexible;
              KEY : key flexible;
              PE : pcache-entry flexible;
   
   

   

   state variables  PCACHE : pcache flexible;

   initialization procedure pcache_format#

   if ERR = ESUCCESS

   sequential

   

   crash predicate true

   with crash-neutrality

   

   recovery procedure pcache_recovery#

   if ERR = ESUCCESS

   declarations format:pcache_format#(; ; PCACHE, ERR)  precondition true;  postcondition true;{{PCACHE := ∅; ERR := ESUCCESS}}
                recovery:pcache_recovery#(; ; PCACHE, ERR)  precondition true;  postcondition true;{{PCACHE := ∅; ERR := ESUCCESS}}
                get:
                pcache_get#(INO, PAGENO, PCACHE; HIT, BUF, ERR)
                  precondition true;
                  postcondition true;
                {{let KEY = datakey(INO, PAGENO) in if KEY ∈ PCACHE then let PE = PCACHE[KEY] in {BUF := PE.page; HIT := true} else HIT := false; 
                  ERR := ESUCCESS}
                }
                set:
                pcache_set#(INO, PAGENO, BUF, DIRTY; ERR, PCACHE)
                  precondition true;
                  postcondition true;
                {let KEY = datakey(INO, PAGENO), PE = mkpentry(DIRTY, BUF) in PCACHE[KEY] := PE
                }
                check-page:
                pcache_check_page#(INO, PAGENO, PCACHE; HIT, DIRTY, ERR)
                  precondition true;
                  postcondition true;
                {let KEY = datakey(INO, PAGENO) in if KEY ∈ PCACHE then {HIT := true; DIRTY := PCACHE[KEY].dirty} else HIT := false
                }
                set-status:
                pcache_set_status#(INO, PAGENO, DIRTY; ERR, PCACHE)
                  precondition true;
                  postcondition true;
                {let KEY = datakey(INO, PAGENO), PE = ?
                 in if KEY ∈ PCACHE then {PE := PCACHE[KEY]; PE := mkpentry(DIRTY, PE.page); PCACHE[KEY] := PE} else ERR := EFAIL
                }
                delete:
                pcache_delete#(INO, PAGENO; ERR, PCACHE)
                  precondition true;
                  postcondition true;
                {let KEY = datakey(INO, PAGENO) in PCACHE := PCACHE -- KEY
                }
                evict:
                pcache_evict#(INO; ERR, PCACHE)
                  precondition ∀ key. key ∈ PCACHE → key.data?;
                  postcondition ∀ key. key ∈ PCACHE → key.data? ∧ key.ino ≠ INO;
                {if ∀ key. key ∈ PCACHE → key.data? then PCACHE := evict(INO, PCACHE) else abort
                }
                truncate:
                pcache_truncate#(INO, SIZE, N; ERR, PCACHE)
                  precondition ∀ key. key ∈ PCACHE → key.data?;
                  postcondition ∀ key. key ∈ PCACHE → key.data? ∧ (key.ino = INO → key.part * VFS_PAGE_SIZE < min(N, SIZE));
                {if ∀ key. key ∈ PCACHE → key.data? then PCACHE := truncate(INO, min(N, SIZE), PCACHE) else abort
                }
end data asm specification