6.826—Principles of Computer Systems 2006 Handout 19. Sequential Transactions with Caching 1 19. Sequential Transactions with Caching There are many situations in which we want to make a ‘big’ action atomic, either with respect to concurrent execution of other actions (everyone else sees that the big action has either not started or run to completion) or with respect to failures (after a crash the big action either has not started or has run to completion). Some examples: Debit/credit: x := x + ∆; y := y – ∆ Reserve airline seat Rename file Allocate file and update free space information Schedule meeting: room and six participants Prepare report on one million accounts Why is atomicity important? There are two main reasons: 1. Stability: A large persistent state is hard to fix it up if it gets corrupted. This can happen because of a system failure, or because an application fails in the middle of updating the state (presumably because of a bug). Manual fixup is impractical, and ad-hoc automatic fixup is hard to code correctly. Atomicity is a valuable automatic fixup mechanism. 2. Consistency: We want the state to change one big action at a time, so that between changes it is always ‘consistent’, that is, it always satisfies the system’s invariant and always reflects exactly the effects of all the big actions that have been applied so far. This has several advantages: • When the server storing the state crashes, it’s easy for the client to recover. • When the client crashes, the state remains consistent. • Concurrent clients always see a state that satisfies the invariant of the system. It’s much easier to code the client correctly if you can count on this invariant. The simplest way to use the atomicity of transactions is to start each transaction with no volatile state. Then there is no need for an invariant that relates the volatile state to the stable state between atomic actions. Since these invariants are the trickiest part of easy concurrency, getting rid of them is a major simplification. Overview In this handout we treat failures without concurrency; handout 20 treats concurrency without failures. A grand unification is possible and is left as an exercise, since the two constructions are more or less orthogonal. We can classify failures into four levels. We show how to recover from the first three. Transaction abort: not really a failure, in the sense that no work is lost except by request. 6.826—Principles of Computer Systems 2006 Handout 19. Sequential Transactions with Caching 2 Crash: the volatile state is lost, but the only effect is to abort all uncommitted transactions. Media failure: the stable state is lost, but it is recovered from the permanent log, so that the effect is the same as a crash. Catastrophe or disaster: the stable state and the permanent log are both lost, leaving the system in an undefined state. We begin by repeating the SequentialTr spec and the LogRecovery code from handout 7 on file systems, with some refinements. Then we give much more efficient code that allows for caching data; this is usually necessary for decent performance. Unfortunately, it complicates matters considerably. We give a rather abstract version of the caching code, and then sketch the concrete specialization that is in common use. Finally we discuss some pragmatic issues. The spec An A is an encoded action, that is, a transition from one state to another that also returns a result value. Note that an A is a function, that is, a deterministic transition. MODULE NaiveSequentialTr [ V, % Value of an action S WITH { s0: ()->S } % State, s0 initially ] EXPORT Do, Commit, Crash = TYPE A = S->(V, S) % Action VAR ss := S.s0() % stable state vs := S.s0() % volatile state APROC Do(a) -> V = << VAR v | (v, vs) := a(vs); RET v >> APROC Commit() = << ss := vs >> APROC Crash () = << vs := ss >> % ‘aborts’ the transaction END NaiveSequentialTr Here is a simple example, with variables X and Y as the stable state, and x and y the volatile state. Action X Y x y 5 5 5 5 Do(x := x – 1); 5 5 4 5 Do(y := y + 1) 5 5 4 6 Commit 4 6 4 6 Crash before commit 5 5 5 5 If we want to take account of the possibility that the server (specified by this module) may fail separately from the client, then the client needs a way to detect this. Otherwise a server failure and restart after the decrement of x in the example could result in X = 5, Y = 6, because the client will continue with the decrement of y and the commit. Alternatively, if the client fails at that point, restarts, and repeats its actions, the result would be X = 3, Y = 6. To avoid these problems,6.826—Principles of Computer Systems 2006 Handout 19. Sequential Transactions with Caching 3 we introduce a new Begin action to mark the start of a transaction as Commit marks the end. We use another state variable ph (for phase) that keeps track of whether there is an uncommitted transaction in progress. A transaction in progress is aborted whenever there is a crash, or if another Begin action is invoked before it commits. We also introduce an Abort action so the client can choose to abandon a transaction explicitly. This exported interface is slightly redundant, since Abort = Begin; Commit, but it’s the standard way to do things. Note that Crash = Abort also; this is not redundant, since the client can’t call Crash. MODULE SequentialTr [ V, % Value of an action S WITH { s0: ()->S } % State; s0 initially ] EXPORT Begin, Do, Commit, Abort, Crash = TYPE A = S->(V, S) % Action VAR ss := S.s0() % Stable State vs := S.s0() % Volatile State ph : ENUM[idle, run] := idle % PHase (volatile) EXCEPTION crashed APROC Begin() = << Abort(); ph := run >> % aborts any current trans. APROC Do(a) -> V RAISES {crashed} = << IF ph = run => VAR v | (v, vs) := a(vs); RET v [*] RAISE crashed FI >> APROC Commit() RAISES {crashed} = << IF ph = run => ss := vs; ph := idle [*] RAISE crashed FI >> APROC Abort () = << vs := ss; ph := idle >> % same as Crash APROC Crash () = << vs := ss; ph := idle >> % ‘aborts’ the transaction END SequentialTr Here is the previous example extended with the ph variable. Action X Y x y ph 5 5 5 5 idle Begin(); 5 5 5 5 run Do(x := x - 1); 5 5 4 5 run Do(y := y + 1) 5 5 4 6 run Commit 4 6 4 6 idle Crash before commit 5 5 5 5 idle 6.826—Principles of Computer Systems 2006 Handout 19. Sequential