abusing your memory model for fun and profit what memory model should rust use

John regehr thread Really good Is Parallel Programming Hard, And, If So, What Can You Do About It? list of kernel data races Herlihy is discussed as a given? concurrency state models and jabva programsd little book of semaphors kernel memory corruption bug from data race prokject zero Concurrent Programming (Andrews) – uses pseudo-code with synchronization/concurrency notation. Transactional Memory (Harris) – for non-lock based concurrency. an introduction to lockless algorithms “Shared-Memory Synchronization” by Michael Scott GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation Weak memory models? - algorithms for scababe synchronization on shared-memory. Same Michiael Scott. BBN butterfly? HOGWILD - parallizingf lock free SGD A Primer on Memory Consistency and Cache Coherence cooperating seauentail prcoesses by dikstra ohearn resources concurrency and local reasoning monitors and concrurent pacscal hitsotry - per brinch hansen “ atomic “release and sleep” is the key as far as I’m concerned, it’s so easy to invent bad solutions without that primitive” the 12 commandments of synchrnonizatiojn

Concurrency Mutex Lock Concurrent hash table barriers - bartosz on c++11 concurrency

pthread vs std::thread Arc in rust condition variables

C++/Java/Ocaml memory models - interesting thesis too hans boehm link farm - “impossible as a library” - mathematizzing C++ memory model, kodkod, isabelle

Various kinds of relations.

futex - fats userspace mutex

lockless algorithsm MPI Cilk OpenMP

rust model checker actor system thing

Leslie lamport

Lindsey kuper has a dist sys course It’s probably pretty good

Lecture 1. several node,s connected by network, characterized by partial failure cloud vs hpc cloud treat failure as expected and work around it “Eveerything fails all tyhe timne” - werner vogels hpc- partial is total failure. checkpointing

M1 -> M2 x? Posslbe problems:

  1. lost request
  2. request from M1 is slow
  3. M2 crashes
  4. M2 slow to respond
  5. seponse is slow
  6. response could get lost
  7. corrupt - byzantine faults.

important: send request to another node and don’t receive a response, it is impossible for you to know why

How do real systems cope? Timeout - wait a certain amount of time then assume failure - imperfect solutuojn

max delay d. max process time r. cn’t really do this asynchronous network - no max Palvaro - partiasl failure + unbounded latency - dedalus - datalog in time and space. bloom blazes, data lineage multiple proofs are fault tolerant. lineage. Why did happen: produce explanation / proof. Cegis? concolic kind of? observability.

kyle kingsbury

chaos engineering - nora jones netflix

Lecture 2 - kuper

clocks. scheduling. intervals in time time of day clocks, monotonic clocks NTP network time protocl. not so good for measuring inervals. can jump forward or backward cloudflare leap second bug monotonic - only goes forward

import time time.monotonic() . not comparable between machines

logical clocks only measuring order of events. A can cause B, not vie versa lamport diagrams/ spacetime daigrams

network models synhcrnous network is one where exists an n such no message takes longer than n asynchrnous - one where the is no n such that no message takes longer than n units “partially synchrnous” n exists but you don’t know what it is

happens before - on same process. if a is send,, and b is receive, then a is before c, trasntivity concurrent - not ordered

state -

mate soos talking about adding mpi z3 had mpi but was disabled. armin biere talking about pthreads - pligenling uses pthreads