ivy/test/ibm-cache-N_mc.ivy

#lang ivy1.7

type client

type message1 = { empty1 , reqshared , reqexclusive }

type message2_4 = { empty2_4 , invalidate , grantshared , grantexclusive }

type message3 = { empty3 , invalidateAck }

type cachestate = { invalid , shared , exclusive }

object s = {
    var channel1(C:client) : message1
    var channel2_4(C:client) : message2_4
    var channel3(C:client) : message3
    var cache(C:client) : cachestate
    var homeSharerList(C:client) : bool
    var homeinvalidateList(C:client) : bool
    var homeexclusiveGranted : bool
    var homeCurrentCommand : message1
    var homeCurrentclient : client
}

var owner : client

after init {
    s.channel1(C) := empty1;
    s.channel2_4(C) := empty2_4;
    s.channel3(C) := empty3;
    s.cache(C) := invalid;
    s.homeSharerList(C) := false;
    s.homeinvalidateList(C) := false;
    s.homeexclusiveGranted := false;
    s.homeCurrentCommand := empty1;
}

action reqsharedRule(cl:client) = {
    require s.cache(cl) = invalid & s.channel1(cl) = empty1;
    s.channel1(cl) := reqshared;
}

action reqexclusiveRule(cl:client) = {
    require (s.cache(cl) = invalid | s.cache(cl) = shared) & s.channel1(cl) = empty1;
    s.channel1(cl) := reqexclusive;
}

action pickNewRequestRule(cl:client) = {
    require s.homeCurrentCommand = empty1 & s.channel1(cl) ~= empty1;
    s.homeCurrentCommand := s.channel1(cl);
    s.channel1(cl) := empty1;
    s.homeCurrentclient := cl;
    s.homeinvalidateList(C) := s.homeSharerList(C);
}

action sendinvalidateRule(cl:client) = {
    require s.channel2_4(cl) = empty2_4 & s.homeinvalidateList(cl)
    & (s.homeCurrentCommand = reqexclusive
    | (s.homeCurrentCommand = reqshared & s.homeexclusiveGranted));
    s.channel2_4(cl) := invalidate;
    s.homeinvalidateList(cl) := false;
}


action receiveinvalidateAckRule(cl:client) = {
    require s.homeCurrentCommand ~= empty1 & s.channel3(cl) = invalidateAck;
    s.homeSharerList(cl) := false;
    s.homeexclusiveGranted := false;
    s.channel3(cl) := empty3;
}

action sharerinvalidatescacheRule(cl:client) = {
    require s.channel2_4(cl) = invalidate & s.channel3(cl) = empty3;
    s.channel2_4(cl) := empty2_4;
    s.channel3(cl) := invalidateAck;
    s.cache(cl) := invalid;
}

action receivesharedGrantRule(cl:client) = {
    require s.channel2_4(cl) = grantshared;
    s.cache(cl) := shared;
    s.channel2_4(cl) := empty2_4;
}

action receiveexclusiveGrantRule(cl:client) = {
    require s.channel2_4(cl) = grantexclusive;
    s.cache(cl) := exclusive;
    s.channel2_4(cl) := empty2_4;
}

action grantsharedRule = {
    require s.homeCurrentCommand = reqshared
    & ~ s.homeexclusiveGranted
    & s.channel2_4(s.homeCurrentclient) = empty2_4;
    s.homeSharerList(s.homeCurrentclient) := true;
    s.homeCurrentCommand := empty1;
    s.channel2_4(s.homeCurrentclient) := grantshared;
}

action grantexclusiveRule = {
    require s.homeCurrentCommand = reqexclusive
    & s.channel2_4(s.homeCurrentclient) = empty2_4 &
    forall I. ~s.homeSharerList(I);
    s.homeSharerList(s.homeCurrentclient) := true;
    s.homeCurrentCommand := empty1;
    s.homeexclusiveGranted := true;
    s.channel2_4(s.homeCurrentclient) := grantexclusive;
    owner := s.homeCurrentclient; 
}



invariant forall C1, C2. C1 ~= C2 & s.cache(C1) = exclusive -> s.cache(C2) = invalid

invariant s.homeexclusiveGranted & s.homeCurrentCommand ~= empty1 & s.channel3(C1) = invalidateAck -> C1 = owner

schema trans1 = {
    type t
    function x : t
    function z : t
    property x = X & z = X -> x = z
}

schema trans2 = {
    type t
    function x : t
    property x = X & Y = X -> x = Y
}

schema cong1 = {
    type t
    type u
    function x : t
    function f(X:t) : u
    property x = X -> f(x) = f(X)
}

schema cong2 = {
    type t1
    type t2
    type u
    function x1 : t1
    function x2 : t2
    function f(X1:t1,X2:t2) : u
    property x1 = X1 & x2 = X2 -> f(x1,x2) = f(X1,X2)
}


export reqsharedRule
export reqexclusiveRule
export pickNewRequestRule
export receiveexclusiveGrantRule
export sendinvalidateRule
export sharerinvalidatescacheRule
export receiveinvalidateAckRule
export grantexclusiveRule
export receivesharedGrantRule
export grantsharedRule