Data Race Free Synchronization Model

  • Description
  • HyTech Code for the associated EFSM (see full paper)

    Description
    DRF
    Data Race Free Synchronization Model (from F.Pong and M.Dubois "Formal Verification of Delayed Consistency Protocols" IPPS96).

    HyTech Code
    --- DATA RACE FREE EXECUTION MODEL
    
    var  out,cs,scs:discrete;
    
    automaton p
    synclabs : ;
    
    initially ss & True;
               
    loc ss : while out >= 0 & scs >=0 & cs >=0 wait {} 
             when 
               out >=1 & cs=0 & scs=0
             do {out'=out-1,cs'=cs+1} goto ss;
             when 
               out >=1 & cs=0 & scs>=0
             do {out'=out-1,scs'=scs+1} goto ss;
             when 
               cs>=1 
             do {out'=out+1,cs'=cs-1} goto ss;
             when 
               scs>=1 
             do {out'=out+1,scs'=scs-1} goto ss;
    end
    
    var 
       init_reg, final_reg, reached, old, new, Aux : region;
    
    init_reg  := loc[p]=ss & out>=1 & cs=0 & scs=0;
    final_reg := loc[p]=ss & cs>=1 & scs>=1;
    
     reached:= reach backward from final_reg endreach;
    --  reached:= reach forward  from init_reg  endreach;
      print reached;