Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
1
Haskell Concurrency and STM
Christine Rizkallah
CSE, UNSW Term 3 2020
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Shared Data Consider the Readers and Writers problem:
Problem
We have a large data structure (i.e. a structure that cannot be updated in one atomic step) that is shared between some number of writers who are updating the data structure and some number of readers who are attempting to retrieve a coherent copy of the data structure.
Desiderata:
We want atomicity, in that each update happens in one go, and updates-in-progress or partial updates are not observable.
We want consistency, in that any reader that starts after an update finishes will see that update.
We want to minimise waiting.
2
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
A Crappy Solution
Treat both reads and updates as critical sections — use any old critical section solution (locks, etc.) to sequentialise all reads and writes to the data structure.
Observation
Updates are atomic and reads are consistent — but reads can’t happen concurrently, which leads to unnecessary contention.
3
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
A Better Solution
A more elaborate locking mechanism (condition variables) could be used to to allow multiple readers to read concurrently, but writers are still executed individually and atomically.
Observation
We have atomicity and consistency, and now multiple reads can execute concurrently. Still, we don’t allow updates to execute concurrently with reads, to prevent partial updates from being observed by a reader.
4
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Reading and Writing
Complication
5
Now suppose we don’t want readers to wait (much) while an update is performed. Instead, we’d rather they get an older version of the data structure.
Trick: Rather than update the data structure in place, a writer creates their own local copy of the data structure, and then merely updates the (shared) pointer to the data structure to point to their copy.
Atomicity The only shared write is now just to one pointer.
Consistency Reads that start before the pointer update get the older version, but reads that start after get the latest.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Persistent Data Structures
Copying is O(n) in the worst case, but we can do better for many tree-like types of data structure.
Example (Binary Search Tree)
Pointer
64
64
37
37
102
20
40
40
6
3
22
42
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
7
Purely Functional Data Structures
Persistent data structures that exclusively make use of copying over mutation are called purely functional data structures. They are so called because operations on them are best expressed in the form of mathematical functions that, given an input structure, return a new output structure:
insert v Leaf = Branch v Leaf Leaf insertv(Branchxlr) = ifv≤xthen
Branch x (insert v l) r else
Branch x l (insert v r)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
8
Computing with Functions
We model real processes in Haskell using the IO type. We’ll treat IO as an abstract type for now, and give it a formal semantics later if we have time:
IO τ = A (possibly effectful) process that, when executed, produces a result of type τ
Note the semantics of evaluation and execution are different things.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Recall monads:
Building up IO
return :: ∀a. a → IO a
(≫=) :: ∀a b. IO a → (a → IO b) → IO b
getChar :: IO Char putChar :: Char → IO ()
echo :: IO ()
echo = getChar ≫= (λx. putChar x ≫= λy. echo)
Example (Echo)
9
Or, with do notation:
echo :: IO () echo = do
x ← getChar putChar x echo
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Adding Concurrency
We can have multiple threads easily enough:
forkIO :: IO () → IO ()
Example (Dueling Printers)
let loop c = do putChar c;loop c in do forkIO (loop ‘a’); loop ‘z’
But what sort of synchronisation primitives are available?
10
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
MVars
The MVar is the simplest synchronisation primitive in Haskell. It can be thought of as a shared box which holds at most one value.
Processes must take the value out of a full box to read it, and must put a value into an empty box to update it.
MVar Functions
newMVar :: ∀a. a → IO (MVar a) takeMVar :: ∀a. MVar a → IO a putMVar :: ∀a. MVar a → a → IO ()
Create a new MVar Read/remove the value Update/insert a value
11
Taking from an empty MVar or putting into a full one results in blocking. An MVar can be thought of as channel containing at most one value.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
12
Readers and Writers
We can treat MVars as shared variables with some definitions:
writeMVar m v = do takeMVar m; putMVar m v
readMVar m = do v ← takeMVar m; putMVar m v ; return v
problem :: DB → IO () problem initial = do
db ← newMVar initial
wl ← newMVar ()
let reader = readMVar db ≫= · · · let writer = do
takeMVar wl
d ← readMVar db let d′ = update d evaluate d′ writeMVar db d′ putMVar wl ()
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
13
Fairness
Each MVar has an attached FIFO queue, so GHC Haskell can ensure the following fairness property:
No thread can be blocked indefinitely on an MVar unless another thread holds that MVar indefinitely.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
The Problem with Locks
Problem
14
Write a procedure to transfer money from one bank account to another. To keep things simple, both accounts are held in memory: no interaction with databases is required. The procedure must operate correctly in a concurrent program, in which many threads may call transfer simultaneously. No thread should be able to observe a state in which the money has left one account, but not arrived in the other (or vice versa).
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
15
The Problem with Locks
Assume some infrastructure for accounts:
type Balance = Int
type Account = MVar Balance
withdraw :: Account → Int → IO ()
withdraw a m = takeMVar a ≫= (putMVar a ◦ subtract m)
deposit :: Account → Int → IO () deposit a m = withdraw a (−m)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Attempt #1
transfer f t m = do withdraw f m; deposit t m
Problem
The intermediate states where a transaction has only been partially completed are externally observable.
In a bank, we might want the invariant that at all points during the transfer, the total amount of money in the system remains constant. We should have no money go missinga .
aWe’re not CBA
16
Readers and Writers
Haskell
Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Attempt #2
transfer f t m = do fb ← takeMVar f tb ← takeMVar t
putMVar t (tb + m) putMVar f (fb − m)
Problem
17
We can have deadlock here, when two people transfer to each other simultaneously and both transfers proceed in lock-step.
Also, not being able to compose our existing withdrawal and deposit operations is unfortuitous from a software design perspective.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
18
Solution
We should enforce a global ordering of locks.
type Account = (MVar Balance, AccountNo)
transfer (f,fa)(t,ta)m=do (fb, tb) ← if fa ≤ ta
then do
fb ← takeMVar f tb ← takeMVar t pure (fb,tb)
else do
tb ← takeMVar t fb ← takeMVar f pure (fb,tb)
putMVar t (tb + m) putMVar f (fb − m)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
It Gets Complicated
Problem
19
Now suppose that some accounts can be configured with a “backup” account that is withdrawn from if insufficient funds are available in the normal account.
Should you take the lock for the backup account?
To make life even harder: What if we want to block if insufficient funds are available?
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
20
Conclusion
Lock-based methods have their place, but from a software engineering perspective they’re a nightmare.
Remember not to take too many locks.
Remember not to take too few locks.
Remember what locks correspond to each piece of shared data.
Remember not to take the locks in the wrong order.
Remember to deal with locks when an error occurs.
Remember to signal condition variables and release locks at the right time.
Most importantly, modular programming becomes impossible.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
The Solution
Represent an account as a simple shared variable containing the balance.
transfer f t m = atomically $ do withdraw f m
deposit t m
Where atomically P guarantees:
Atomicity The effects of the action P become visible all at once.
Isolation The effects of action P is not affected by any other threads.
Problem
How can we implement atomically?
21
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
The Global Lock
We can adopt the solution of certain reptilian programming languages.
Problem
Atomicity is guaranteed, but what about isolation? Also, performance is predictably garbage.
22
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
23
Ensuring Isolation
Rather than use regular shared variables, use special transactional variables.
:: a → STM (TVar a)
:: TVar a → STM a
:: TVar a → a → STM ()
:: STM a → IO a
The type constructor STM is also an instance of the Monad type class, and thus
supports the same basic operations as IO.
pure :: a → STM (TVar a)
(≫=) :: STMa→(a→STMb)→STMb
createTVar readTVar writeTVar
atomically
Readers and Writers
Haskell
Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
24
Implementing Accounts
type Account = TVar Int
withdraw :: Account → Int → STM () withdraw a m = do
balance ← readTVar m writeTVar a (balance − m)
deposit a m = withdraw a (−m)
Observe: withdraw (resp. deposit) can only be called inside an atomically ⇒ We
have isolation.
But, we’d still like to run more than one transaction at once — one global lock isn’t good enough.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Optimistic Execution
Each transaction (atomically block) is executed optimistically. This means they do not need to check that they are allowed to execute the transaction first (unlike, say, locks, which prefer a pessimistic model).
Implementation Strategy
Each transaction has an associated log, which contains:
The values written to any TVars with writeTVar.
The values read from any TVars with readTVar, consulting earlier log entries first.
First the log is validated, and, if validation succeeds, changes are committed. Validation and commit are one atomic step.
What can we do if validation fails? We re-run the transaction!
25
Readers and Writers
Haskell
Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
26
Re-running transactions
atomically $ do
x ← readTVar xv
y ← readTVar yv
if x > y then launchMissiles else pure ()
To avoid serious international side-effects, the transaction must be repeatable. We can’t change the world until commit time.
A real implementation is smart enough not to retry with exactly the same schedule.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Blocking and retry We want to block if insufficient funds are available.
We can use the helpful action retry :: STM a.
withdraw′ :: Account → Int → STM () withdraw′ a m = do
balance ← readTVar a ifm>0&&m>balance then
retry
else
writeTVar a (balance − m)
Problem
27
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Choice and orElse
Problem
28
We want to transfer from a backup account if the first account has insufficient funds, and block if neither account has insufficient funds.
We can use the helpful action
orElse :: STM a → STM a → STM a
wdBackup :: Account → Account → Int → STM ()
wdBackup a1 a2 m = orElse (withdraw′ a1 m) (withdraw′ a2 m)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
29
Evaluating STM
STM is modular. We can compose transactions out of smaller transactions. We can hide concurrency behind library boundaries without worrying about deadlock or global invariants.
Lock-free data structures and transactional memory based solutions work well if contention is low and under those circumstances scale better to higher process numbers than lock-based ones.
Most importantly, the resulting code is often simpler and more robust. Profit!
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
30
Progress
One transaction can force another to abort only when it commits.
At any time, at least one currently running transaction can successfully commit.
Traditional deadlock scenarios are impossible, as is cyclic restarting where two transactions constantly cancel each other.
Starvation is possible (when?), however uncommon in practice. So, we technically don’t have eventual entry.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
31
Performance
A concurrent channel using STM was implemented and compared to an MVar version. The STM version performs within 10% of the MVar version, and uses half of the heap space −→ Profit! 1
The implementation is a bit simpler as well. Let’s do it if we have time! Just a linked list, really.
1Mostly, the MVar implementation performed poorly due to lots of overhead to make it exception-safe.
Readers and Writers
Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
32
Atomicity Consistency
Isolation Durability
Each transaction should be ‘all or nothing’.
Each transaction in the future sees the effects of transactions in the
past.
The transaction’s effect on the state cannot be affected by other transactions.
The transaction’s effect on the state survives power outages and crashes.
Database Guarantees
STM gives you 75% of a database system. The Haskell package acid-state builds on STM to give you all four.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
33
Hardware Transactional Memory
The latest round of Intel processors support Hardware Transactional Memory instructions:
XBEGIN
XEND
XTEST
XABORT
Begin a hardware transaction
End a hardware transaction
Test if currently executing a transaction.
Abort the transaction and jump to the abort handler.
The “log” we described earlier is stored in L1 cache. Speculative writes are limited to the amount of cache we have. If a speculative read overflows the cache, it may sometimes generate a spurious conflicts and cause the transaction to abort.
For this reason, progress can only be ensured through the combination of STM and HTM. Work is currently underway to implement this for Haskell, and prototypes show promising performance improvements.
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
34
That’s it
We have now covered all the content in COMP3161/COMP9164. Thanks for sticking with the course.
Syntax Foundations
Concrete/Abstract Syntax, Ambiguity, HOAS, Binding, Variables, Substitution, λ-calculus
Semantics Foundations
Static Semantics, Dynamic Semantics (Small-Step/Big-Step), Abstract Machines, Environments, Stacks, Safety, Liveness, Type Safety (Progress and Preservation) Features
Algebraic Data Types, Recursive Types Exceptions
Polymorphism, Type Inference, Unification Overloading, Subtyping, Abstract Data Types Concurrency, Critical Sections, STM
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
MyExperience
https://myexperience.unsw.edu.au
35
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
36
Further Learning
UNSW courses:
COMP3141 — Software System Design and Implementation
COMP6721 — (In-)formal Methods
COMP3131 — Compilers
COMP4141 — Theory of Computation COMP6752 — Modelling Concurrent Systems COMP3151 — Foundations of Concurrency COMP4161 — Advanced Topics in Verification COMP3153 — Algorithmic Verification
Online Learning
Oregon Programming Languages Summer School Lectures
(https://www.cs.uoregon.edu/research/summerschool/archives.html) Videos are available from here! Also some on YouTube.
Bartosz Milewski’s Lectures on Category Theory are on YouTube.
Books — see Liam’s Book List!
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
37
The exam is on Tuesday, 8th of December 2020 at 2pm. I have posted a sample exam with revision questions. The final exam will run similar to the sample exam.
It runs for 2 hours and 10 minutes.
What’s next?
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
38
Evaluation Semantics
The semantics of Haskell’s evaluation are interesting but not particularly relevant for us. We will assume that it happens quietly without a fuss:
β-equivalence α-equivalence η-equivalence
(λx. M[x]) N λx. M[x]
λx. M x
≡β M[N] ≡α λy. M[y] ≡η M
Let our ambient congruence relation ≡ be ≡αβη enriched with the following extra equations, justified by the monad laws:
returnN≫=M ≡MN
(X≫=Y)≫=Z ≡ X≫=(λx.Yx≫=Z) X ≡ X≫=return
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Processes
This means that a Haskell expression of type IO τ for will boil down to either return x where x is a value of type τ; or a ≫= M where a is some primitive IO action
(forkIO p, readMVar v, etc.) and M is some function producing another IO τ. This is the head normal form for IO expressions.
Definition
Define a language of processes P, which contains all (head-normal) expressions of type IO ().
We want to define the semantics of the execution of these processes. Let’s use operational semantics:
(→) ⊆ P × P
39
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
40
Semantics for forkIO
To model forkIO, we need to model the parallel execution of multiple processes in our process language. We shall add a parallel composition operator to the language of processes:
P,Q ::= a≫=M | return ()
| P∥Q | ···
And the following ambient congruence equations:
P∥Q ≡ Q∥P P∥(Q∥R) ≡ (P∥Q)∥R
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Semantics for forkIO
If we have multiple processes active, pick one of them non-deterministically to move:
P → P′
P ∥ Q → P′ ∥ Q
The forkIO operation introduces a new process:
(forkIOP≫=M) → P∥(return()≫=M)
41
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
42
Semantics for MVars
MVars are modelled as a special type of process, identified by a unique name. Values of MVar type merely contain the name of the process, so that putMVar and friends know where to look.
P,Q ::= a≫=M
|
|
|
| ···
return () P∥Q
⟨⟩n | ⟨v⟩n
⟨⟩n ∥ (putMVar n v ≫=M) → ⟨v⟩n ∥ (return ()≫=M) ⟨v⟩n ∥ (takeMVar n ≫= M) → ⟨⟩n ∥ (return v ≫= M)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Semantics for newMVar
We might think that newMVar should have semantics like this: (newMVar v ≫= M) → ⟨v⟩n ∥ (return n ≫= M)(n fresh)
But this approach has a number of problems:
The name n is now globally-scoped, without an explicit binder to introduce it.
It doesn’t accurately model the lifetime of the MVar, which should be garbage-collected once all processes that can access it finish.
It makes MVars global objects, so our semantics aren’t very abstract. We would like local communication to be local in our model.
43
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
44
Restriction Operator
We introduce a restriction operator ν to our language of processes:
P,Q ::= a≫=M
| return ()
| P∥Q
| ⟨⟩n | ⟨v⟩n
| (νn)P
Writing (ν n) P says that the MVar name n is only available in process P. Mentioning n outside P is not well-formed. We need the following additional congruence equations:
(νn)(νm)P ≡ (νm)(νn)P (νn)(P∥Q) ≡ P∥(νn)Q (ifn∈/P)
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Better Semantics for newMVar
The rule for newMVar is much the same as before, but now we explicitly restrict the MVar to M.
(newMVar v ≫= M) → (ν n)(⟨v⟩n ∥ (return n ≫= M))(n fresh) We can always execute under a restriction:
P → P′
(ν n) P → (ν n) P′
Question
What happens when you put an MVar inside another MVar?
45
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
46
Garbage Collection
If an MVar is no longer used, we just replace it with the do-nothing process:
(ν n) ⟨⟩n → return () (ν n) ⟨v⟩n → return ()
Extra processes that have outlived their usefulness disappear:
return()∥P → P
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Process Algebra
Our language P is called a process algebra, a common means of describing semantics for concurrent programs.
Process algebras and calculi of various kinds are covered in great detail in COMP6752 with Rob van Glabbeek, who is an expert in this field.
If there’s time!
We can talk about more concurrency topics.
47
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Simon Marlow
Bibliography
Parallel and Concurrent Programming in Haskell
O’Reilly, 2013
http://chimera.labs.oreilly.com/books/1230000000929
Simon Peyton Jones, Andrew Gordon and Sigbjorn Finne
Concurrent Haskell
POPL ’96
Association for Computer Machinery
http://microsoft.com/en- us/research/wp- content/uploads/1996/01/concurrent- haskell.pdf
Simon Marlow (Editor)
Haskell 2010 Language Report
https://www.haskell.org/onlinereport/haskell2010/
48
Readers and Writers Haskell Issues with Locks Software Transactional Memory Wrap-up Bonus: Semantics for IO
Bibliography
Simon Peyton Jones
Beautiful Concurrency
49
In “Beautiful Code”, ed. Greg Wilson, O’Reilly, 2007
http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/beautiful.pdf
Tim Harris, Simon Marlow, Simon Peyton Jones, Maurice Herlihy
Composable Memory Transactions
PPoP ’05
Association for Computer Machinery www.microsoft.com/en-us/research/wp-content/uploads/2005/01/2005-ppopp-composable.pdf
David Himmelstrup
Acid-State Library
https://github.com/acid-state/acid-state
Ryan Yates and Michael L. Scott
A Hybrid TM for Haskell
TRANSACT ’14
Association for Computer Machinery