gterzian

---------------------- MODULE RenderingUpdateBatching ----------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_queue, rendering_task_queued, closed
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ task_queue \in [Pipeline -> BOOLEAN]
          /\ rendering_task_queued \in [Pipeline -> BOOLEAN]
          /\ closed \in SUBSET Pipeline

gterzian

---------------------- MODULE RenderingUpdateBatchingBroken ----------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_queue, rendering_task_queued
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ task_queue \in [Pipeline -> BOOLEAN]
          /\ rendering_task_queued \in BOOLEAN

gterzian

----------------------------- MODULE FGEventLoop ---------------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_state, step_state
CONSTANT N
----------------------------------------------------------------------------

Count == 0..N
Task == {"Other", "Update"}
Step == {"A", "B"}

gterzian

----------------------------- MODULE EventLoop -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_counter, step_counter
CONSTANT N
----------------------------------------------------------------------------

Count == 0..N
Task == {"Other", "Update"}
Step == {"A", "B"}

gterzian

----------------------------- MODULE EventLoop -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_counter, step_counter
CONSTANT N
----------------------------------------------------------------------------

Count == 0..N
Task == {"One", "Two"}
Step == {"A", "B"}

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);