gterzian

/// Implementation of the algorithm described at
/// https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf
use std::collections::HashMap;
use std::sync::{Arc, Mutex};

#[derive(Eq, PartialEq, Hash, Clone)]
struct ProcessId(i32);

#[derive(Debug, Clone)]
enum Value {

gterzian

------------------------ MODULE TeachingConcurrency ------------------------
EXTENDS FiniteSets, Naturals
VARIABLES x, y
CONSTANT N, NoVal
----------------------------------------------------------------------------
\* Specification based on "Teaching Concurrency"
\* found at https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf

Process == 0..(N - 1)

gterzian

enum Consensus {
    MultiPaxos(Vec<Arc<Mutex<Synod>>>),
    ViewStampedReplication(Arc<Mutex<VsrState>>)
}

gterzian

------------------------- MODULE DistributedBakery -------------------------
EXTENDS Naturals, Sequences, FiniteSets
VARIABLES nums, views, in_cs, acks, queues
CONSTANTS N
------------------------------------------------------
Peers == 1..N

AckMsg == N+1
 
TypeOk == /\ nums \in [Peers -> Nat]

gterzian

fn example_with_sequential_mutices(my_thread_mutex_permission: OuterMutexPermission) {
    // We have three sequential mutices. The type system ensures we always
    // claim A then B then C, never C then B then A.
    let can_safely_read = Arc::new(DeadlockProofMutex::new(false, unique_type!()));
    let mutex1 = Arc::new(DeadlockProofMutex::new(0, unique_type!()));
    let mutex2 = Arc::new(DeadlockProofMutex::new(0, unique_type!()));
    let mutex3 = Arc::new(DeadlockProofMutex::new(0, unique_type!()));
    let c_mutex1 = Arc::clone(&mutex1);
    let c_mutex2 = Arc::clone(&mutex2);
    let c_mutex3 = Arc::clone(&mutex3);

gterzian

----------------------------- MODULE Semaphore -----------------------------
EXTENDS Naturals, Sequences
VARIABLES level, clients, queue
CONSTANT UpperBound, ClientId
----------------------------------------------------------------------------

ClientStatus == {"Acquired", "Released", "Waiting", "Cancelled"}

Init == /\ level = UpperBound
        /\ clients = [fut \in ClientId |-> "Released" ]

gterzian

----------------------- MODULE DistributedLockFixed -----------------------
EXTENDS Naturals, Sequences
VARIABLES clients, data_written, last_lock, last_write
CONSTANT ClientId
----------------------------------------------------------------------------

LockStatus == {"NotAcquired", "Acquired"}

Init == /\ clients = [client \in ClientId |-> <<"NotAcquired", 0>> ]
        /\ data_written = [client \in ClientId |-> <<>> ]

gterzian

----------------------- MODULE DistributedLockBroken -----------------------
EXTENDS Naturals, Sequences
VARIABLES clients, lock_checked, data_written
CONSTANT ClientId
----------------------------------------------------------------------------

LockStatus == {"NotAcquired", "Acquired"}

Init == /\ clients = [client \in ClientId |-> "NotAcquired" ]
        /\ lock_checked = [client \in ClientId |-> FALSE ]

gterzian

---------------------- MODULE ArchetypeConcurrencyFix ----------------------

EXTENDS Naturals, Sequences
VARIABLES queue_a, queue_b, received_third, received_second, sent_messages
CONSTANT QLen
ASSUME (QLen \in Nat) /\ (QLen > 1) 
--------------------------------------------------------------

Messages == {"First", "Second", "Third"}

gterzian

---------------------- MODULE ArchetypeConcurrencyBug ----------------------
EXTENDS Naturals, Sequences
VARIABLES queue_a, queue_b, queue_c, received_third, received_second, sent_messages
CONSTANT QLen
ASSUME (QLen \in Nat) /\ (QLen > 0) 
--------------------------------------------------------------

Messages == {"First", "Second", "Third"}

Init == /\ queue_a = << >>