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

Specification FLIT-refines-FLITPSCweak
automaton refinement 
   export FLITPSCweak-proofs
   
   import FLIT-proofs
   
   using abs-FLIT-FLITPSCweak
   abstraction ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters;
   
   local abstraction 
       idle : apc = idle;
      
       ready : apc = ready;
      
       crashed : apc = crashed;
      
       R1 : apc = R1;
      
       R2 : apc = R2;
      
       R3 : apc = R3;
      
       R4 : apc = R4;
      
       R1 -> R4 : loc = l;
      
       R2 -> R4 : val = v;
      
       W1 : apc = W1;
      
       W2 : apc = (SF ∈ bq(t) ⊃ W1;W2);
      
       W3 : apc = W3;
      
       W4 : apc = (W(loc, val) ∈ bq(t) ⊃ W3;W4);
      
       W5 : apc = (W(loc, val) ∈ bq(t) ⊃ W3;(FO(loc) ∈ bq(t) ⊃ W4;W5));
      
       W6 : apc = (W(loc, val) ∈ bq(t) ⊃ W3;(FO(loc) ∈ bq(t) ⊃ W4;(SF ∈ bq(t) ⊃ W5;W6)));
      
       W7 : apc = W7;
      
       W1 -> W7 : loc = l;
      
       W1 -> W7 : val = v;
   
   by action mapping callRUN(t); -> callPSCRUN(t); callFLITCOMPLETE(t); -> callPSCCOMPLETE(t); globalCRASH; -> globalPSCCRASH; 
                     globalPERSIST_W(l); -> globalPSCPERSIST_W(l); globalPERSIST_FO(l); -> globalPSCPERSIST_FO(l); 
                     invFLITREAD(t, l); -> invFLITPSCREAD(t, l); doRead(t, l, v); -> doReadPSC(t, l, v); ctrRead(t, l, n); -> ctrReadPSC(t, l, n); 
                     pwb(t, l); -> pwbPSC(t, l); retFLITREAD(t, v); -> retFLITPSCREAD(t, v); invFLITWRITE(t, l, v); -> invFLITPSCWRITE(t, l, v); 
                     propSF(t); -> sfencePSC(t); ctrInc(t, l); -> ctrIncPSC(t, l); doWrite(t, l, v); -> doWritePSC(t, l, v); 
                     doWriteFO(t, l); -> pwbPSC(t, l); ctrDec(t, l); -> ctrDecPSC(t, l); retFLITWRITE(t); -> retFLITPSCWRITE(t);
   
end automaton refinement