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 = << >>

gterzian

------------------------ MODULE FailingSharedStorage ------------------------
EXTENDS Naturals, Sequences
VARIABLES incoming, outgoing, statuses, shared_storage
CONSTANT QLen, Id
ASSUME (QLen \in Nat) /\ (QLen > 0) 
--------------------------------------------------------------
StoredObject == {"Vacant", "Occupied"}
Statuses == {"Vacant", "Waiting", "Processed"}

Init == /\ shared_storage = [p \in Id |-> "Vacant" ]

gterzian

--------------------------- MODULE SharedStorage ---------------------------
EXTENDS Naturals, Sequences
VARIABLES incoming, outgoing, statuses, shared_storage
CONSTANT QLen, Id
ASSUME (QLen \in Nat) /\ (QLen > 0) 
--------------------------------------------------------------
StoredObject == {"Vacant", "Occupied"}
Statuses == {"Vacant", "Waiting", "Processed"}

Init == /\ shared_storage = [p \in Id |-> "Vacant" ]

gterzian

#[macro_use]
extern crate crossbeam_channel;

use crossbeam_channel::unbounded;
use std::collections::hash_map::Entry;
use std::collections::{HashMap, HashSet};
use std::thread;
use std::time::Duration;
use uuid::Uuid;