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;

gterzian

    // Spawn the "payment" service.
    let _ = thread::spawn(move || loop {
        match payment_request_receiver.recv() {
            Ok(PaymentRequest::NewOrder(order_id)) => {
                // Process the payment for a new order.
                let _ = payment_result_sender.send(PaymentResult(order_id, true));
            }
            Ok(PaymentRequest::ShutDown) => {
                break;
            }

gterzian

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
struct CustomerId(Uuid);

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
struct OrderId(Uuid);

/// Messages sent from the "basket" service,
/// to the "order" service.
enum OrderRequest {
    /// A customer is attempting to make a new order.