Logo Search packages:      
Sourcecode: acl2 version File versions  Download package

ccp.m

Const
  n: 30;

Type
  Msg:   enum { null, req_sh, req_ex, inv, inv_ack, gr_sh, gr_ex };
  State: enum { I, S, E };
  ID:    Scalarset(n);

Var
  ch1: array of Msg;                  /* channel 1 */
  ch2: array of Msg;                  /* channel 2 */
  ch3: array of Msg;                  /* channel 3 */
  hsl: array of boolean;              /* home_shared_list */
  hil: array of boolean;              /* home_invalidate_list */
  heg: boolean;                           /* home_exclusive_granted */
  hcm: Msg;                               /* home_current_command */
  hcc: ID;                                /* home_current_client */
  c:   array of State;                /* distributed cache state */


Ruleset i: ID do

  rule "1" /* client requests shared access */
  c = I & ch1 = null ==>
  begin
    ch1 := req_sh;
  end;

  rule "2" /* client requests exclusive access */
  c = I & ch1 = null ==>
  begin
    ch1 := req_ex;
  end;

  rule "3" /* home picks new request */
  hcm = null & ch1 != null ==>
  begin
    hcm := ch1;
    ch1 := null;
    hcc := i;
    for j: ID do
      hil := hsl;
    end;
  end;

  rule "4" /* home sends invalidate message */
  hil & ch2 = null & ((hcm = req_sh & heg) | hcm = req_ex) ==>
  begin
    ch2 := inv;
    hil := false;
  end;

  rule "5" /* home receives invalidate acknowledgement */
  hcm != null & ch3 = inv_ack ==>
  begin
    hsl := false;
    heg := false;
    ch3 := null;
  end;

  rule "6" /* sharer invalidates cache */
  ch2 = inv & ch3 = null ==>
  begin
    ch2 := null;
    ch3 := inv_ack;
    c := I;
  end;

  rule "7" /* client receives shared grant */
  ch2 = gr_sh ==>
  begin
    c := S;
    ch2 := null;
  end;

  rule "8" /* client receives exclusive grant */
  ch2 = gr_ex ==>
  begin
    c := E;
    ch2 := null;
  end;

end; /* ruleset */

rule "9" /* home grants share */
  hcm = req_sh & !heg & ch2 = null ==>
  begin
    hsl := true;
    hcm := null;
    ch2 := gr_sh;
  end;

rule "10" /* home grants exclusive */
  hcm = req_ex & (forall i: ID do hsl = false end) & ch2[hcc] = null ==>
  begin
    hsl[hcc] := true;
    hcm := null;
    heg := true;
    ch2 := gr_ex;
  end;


startstate
  begin
    for i: ID do
      ch1 := null;
      ch2 := null;
      ch3 := null;
      c := I;
      hsl := false;
      hil := false;
    end;
    hcm := null;
    hcc := undefined;
    heg := false;
  end;

Invariant
  forall i: ID do
    c = E ->
      forall j: ID do
        j != i -> c = I
      end
  end

Generated by  Doxygen 1.6.0   Back to index