gterzian

----------------------------- MODULE RafDelivery -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES raf_requested, tick_received
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in BOOLEAN
  

gterzian

----------------------------- MODULE RafBroken -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES raf_requested, tick_received
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in [Pipeline -> BOOLEAN]
  

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