Specification icache-asm

[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 
   icache

   using cache-base, 
         error-class


   

   
   
   
   
   procedures icache_format#  :  : icache × error  ;
              icache_recovery#  :  : icache × error  ;
              icache_get# nat × icache : bool × inode × error nonfunctional ;
              icache_set# inode × bool : error × icache nonfunctional ;
              icache_check_inode# nat × icache : bool × bool × error nonfunctional ;
              icache_set_status# nat × bool : error × icache nonfunctional ;
              icache_delete# nat : error × icache nonfunctional ;
   variables  ICACHE : icache flexible;
              INO : nat flexible;
              HIT : bool flexible;
              DIRTY : bool flexible;
              INODE : inode flexible;
              IE : icache-entry flexible;
   
   

   

   state variables  ICACHE : icache flexible;

   initialization procedure icache_format#

   if ERR = ESUCCESS

   sequential

   

   crash predicate true

   with crash-neutrality

   

   recovery procedure icache_recovery#

   if ERR = ESUCCESS

   declarations format:icache_format#(; ; ICACHE, ERR)  precondition true;  postcondition true;{{ICACHE := ∅; ERR := ESUCCESS}}
                recovery:icache_recovery#(; ; ICACHE, ERR)  precondition true;  postcondition true;{{ICACHE := ∅; ERR := ESUCCESS}}
                get:
                icache_get#(INO, ICACHE; HIT, INODE, ERR)
                  precondition true;
                  postcondition true;
                {{if INO ∈ ICACHE then {INODE := ICACHE[INO].inode; HIT := true} else HIT := false; ERR := ESUCCESS}
                }
                set:icache_set#(INODE, DIRTY; ERR, ICACHE)  precondition true;  postcondition true;{ICACHE[INODE.ino] := mkientry(DIRTY, INODE)}
                check-inode:
                icache_check_inode#(INO, ICACHE; HIT, DIRTY, ERR)
                  precondition true;
                  postcondition true;
                {if INO ∈ ICACHE then {HIT := true; DIRTY := ICACHE[INO].dirty} else HIT := false
                }
                set-status:
                icache_set_status#(INO, DIRTY; ERR, ICACHE)
                  precondition true;
                  postcondition true;
                {if INO ∈ ICACHE then ICACHE[INO].dirty := DIRTY else ERR := EFAIL
                }
                delete:icache_delete#(INO; ERR, ICACHE)  precondition true;  postcondition true;{ICACHE := ICACHE -- INO}
end data asm specification