SpinLock 实现

/*

 Example: SpinLock

 Description: SpinLock is the lock implementation using AtomicInteger as a primitive synchronizer.

 The contracts is based on the paper to be submitted to ECOOP14.

 These contracts are specified with one abstract predicate for the resource exchange.

 Author: Afshin Amighi

 Status: Pass.

 command: vct --chalice --progress --explicit SpinLock.java

 */

public class SpinLock{

    //shared resource

    private int data;

    //  int SynchronizerRole (S) = 0, ThreadRole = 1;

    //  int UNLOCKED = 0 , LOCKED = 1;

    //@ resource handle(int role,int val);

    //@ resource trans(int role,int last,int next)=( role == 1  ==> true );

    //@ pure zfrac part(int rs,int s,int rt, int v){ return (rs == 0 && s == 0) ? 100:0; }

    // for simplicity we take resource_invariant=Perm(data,p)

    //@ resource inv(zfrac p)= Perm(data,p);

    /* ----------- AtomicInteger -----------------*/

    /*@

     given int r, l;

     requires srh:handle(r,l) ** sra:trans(r,l,v) ** srr:inv(part(0,v,r,v)) ;

     ensures seh:handle(r,v) ** ser:inv(part(0,l,r,l));

     */

    void set(int v);

    /*@

     given int r, l;

     requires crh:handle(r,l) ** cra:trans(r,x,n) ** crr:inv(part(0,n,r,n));

     ensures \result ==> cehp:handle(r,n) ** cerp:inv(part(0,x,r,x));

     ensures !\result ==> cehn:handle(r,l) ** cern:inv(part(0,n,r,n));

     */

    boolean compareAndSet(int x,int n);

    /*----------- SpinLock ----------------*/

    //@ given int last;

    //@ requires lrh: handle(1,last);

    //@ ensures leh: handle(1,1) ** Perm(data,100);

    public void dolock(){

        boolean succ = false;

        //@ int role = 1, S=0;

        //@ SpinLock.trans tcra;

        //@ SpinLock.inv tcrr , tces;

        //@ fold tcrr:inv(part(S,1,role,1));

        //@ loop_invariant  !succ  ==> invhn:handle(role,last) ** invpn: inv(part(S,1,role,1));

        //@ loop_invariant  succ   ==> invhp:handle(role,1) ** invpp: inv(part(S,0,role,0));

        while (!succ) /*@ with{ invhn = lrh;  invpn = tcrr; } then { leh = invhp; tces = invpp;  } */ {

                       //@     fold tcra:trans(role,0,1);

                       succ = compareAndSet(0,1) /*@ with{ r = role; l = last; crh = invhn; cra = tcra; crr = invpn; }

                                                    then{ invhn = cehn; invpn = cern; invhp = cehp; invpp = cerp; } */ ;

                   }

        //@ unfold tces: inv(part(S,0,role,0));

         return;

    }

    //@ requires urh:handle(1,1) ** Perm(data,100);

    //@ ensures ueh: handle(1,0);

    public void unlock(){

        //@ int role = 1, S=0;

        //@ int last = 1;

        //@ SpinLock.inv tsrp;

        //@ fold tsrp:inv(part(S,0,role,0));

        //@ SpinLock.trans tsra;

        //@ fold tsra:trans(role,last,0);

        set(0) /*@ with{ r = role; l = last; srh = urh; sra = tsra; srr = tsrp; } then { ueh = seh; } @*/;

    }

}