How to formally specify a lock in Dafny

final-proof.dfy

newtype ThreadId = i: nat | i <= 0xffff_ffff

class Lock
{
    static const NULL_THREAD_ID : ThreadId := 0

    var ownerThread : ThreadId

    constructor()
        ensures ownerThread == NULL_THREAD_ID
    {
        ownerThread := NULL_THREAD_ID;
    }

    method TryAcquireLock(threadId : ThreadId) returns (success : bool)
        modifies this
        //requires threadId != NULL_THREAD_ID //invalid input
        ensures old(ownerThread) == NULL_THREAD_ID ==> success //can't use IFF because of reentrancy
        ensures success ==> ownerThread == threadId
        ensures success ==> old(ownerThread) in  { NULL_THREAD_ID, threadId } 
    {
        var casResult := CompareAndSwap(NULL_THREAD_ID, threadId);

        return casResult == threadId;
    }

    method ReleaseLock()
        modifies this
        ensures ownerThread == NULL_THREAD_ID
    {
        var casResult := CompareAndSwap(ownerThread, NULL_THREAD_ID);
    }

     method CompareAndSwap(valueToCompare  : ThreadId, valueToSwap : ThreadId) returns (upToDateValue : ThreadId)
        modifies this
        ensures ownerThread == upToDateValue
        ensures old(ownerThread) == valueToCompare ==> upToDateValue == valueToSwap == ownerThread
        ensures old(ownerThread) != valueToCompare ==> ownerThread == old(ownerThread)
    {
        if (ownerThread == valueToCompare)
        {
            ownerThread := valueToSwap;
        }

        return ownerThread;
    }
}

method Main()
{
    var lock := new Lock();

    var thread1Id :| thread1Id > 0;
    var thread2Id :| thread2Id > 0 && thread2Id != thread1Id;

    //thread 1 tries to acquire the lock
    var success := lock.TryAcquireLock(thread1Id);
    assert success;

    //thread 2 tries to acquire the lock
    success := lock.TryAcquireLock(thread2Id);
    assert !success;

    //thread 1 releases the lock
    lock.ReleaseLock();

    //thread 2 tries to acquire the lock
    success := lock.TryAcquireLock(thread2Id);
    assert success;

    //thread 1 tries to acquire the lock again
    success := lock.TryAcquireLock(thread1Id);
    assert !success;
}

starting-proof.dfy

newtype ThreadId = i: nat | i <= 0xffff_ffff

class Lock
{
    const NULL_THREAD_ID : ThreadId := 0

    var ownerThread : ThreadId

    constructor()
    {
        ownerThread := NULL_THREAD_ID;
    }

    method TryAcquireLock(threadId : ThreadId) returns (success : bool)
        modifies this//don't worry about this for now, dafny requires it
    {
        //swap in the current threadId if the lock is free (ownerThread == 0)
        var casResult := CompareAndSwap(NULL_THREAD_ID, threadId);

        //return true if the swap worked
        return casResult == threadId;
    }

    //Should only be called by the actor that holds the lock. This is based on the honor system 😇
    method ReleaseLock()
        modifies this
    {
        //operation should/will always succeed(sorta...)
        var casResult := CompareAndSwap(ownerThread, NULL_THREAD_ID);
    }

    //in reality, we would actually do this with atomic CPU instructions, but for simplicity we pretend it is atomic
     method CompareAndSwap(valueToCompare  : ThreadId, valueToSwap : ThreadId) returns (upToDateValue : ThreadId)
        modifies this
    {
        if (ownerThread == valueToCompare)
        {
            ownerThread := valueToSwap;
        }

        return ownerThread;
    }
}