14 Pages
English

Fault Tolerance via Idempotence

Gain access to the library to view online
Learn more

Description

Fault Tolerance via Idempotence G. Ramalingam and Kapil Vaswani Microsoft Research, India grama,kapilv@microsoft.com Abstract ing comes with its own pitfalls, such as process failures, imperfect messaging, asynchrony and concurrency.Building distributed services and applications is challenging due Consider the prototypical bank account transfer service into the pitfalls of distribution such as process and communication Fig. 1. The goal of the service is to transfer money between bankfailures. A natural solution to these problems is to detect potential accounts, potentially in different banks. If the accounts belong tofailures, and retry the failed computation and/or resend messages. different banks, ensuring that the transfer executes as an atomicEnsuring correctness in such an environment requires distributed (distributed) transaction is usually not feasible, and the natural wayservices and applications to be idempotent. of expressing this computation is as a workflow [10, 20] consistingIn this paper, we study the inter-related aspects of process fail- of two steps, a debit followed by a credit.ures, duplicate messages, and idempotence. We first introduce a What if the process executing the workflow fails in between thesimple core language (based on -calculus) inspired by modern dis- debit and credit steps? A natural solution is to detect this failuretributed computing platforms.

Subjects

Informations

Published by
Published 25 January 2013
Reads 68
Language English

Fault Tolerance via Idempotence
G. Ramalingam and Kapil Vaswani
Microsoft Research, India
grama,kapilv@microsoft.com
Abstract ing comes with its own pitfalls, such as process failures, imperfect
messaging, asynchrony and concurrency.Building distributed services and applications is challenging due
Consider the prototypical bank account transfer service into the pitfalls of distribution such as process and communication
Fig. 1. The goal of the service is to transfer money between bankfailures. A natural solution to these problems is to detect potential
accounts, potentially in different banks. If the accounts belong tofailures, and retry the failed computation and/or resend messages.
different banks, ensuring that the transfer executes as an atomicEnsuring correctness in such an environment requires distributed
(distributed) transaction is usually not feasible, and the natural wayservices and applications to be idempotent.
of expressing this computation is as a workflow [10, 20] consistingIn this paper, we study the inter-related aspects of process fail-
of two steps, a debit followed by a credit.ures, duplicate messages, and idempotence. We first introduce a
What if the process executing the workflow fails in between thesimple core language (based on-calculus) inspired by modern dis-
debit and credit steps? A natural solution is to detect this failuretributed computing platforms. This language formalizes the notions
and ensure that a different process completes the remaining stepsof a service, duplicate requests, process failures, data partitioning, 1of the workflow. A challenging aspect of realizing this solutionand local atomic transactions that are restricted to a single store.
is figuring out whether the original process failed before or afterWe then formalize a desired (generic) correctness criterion for
completing a particular step (either debit or credit). If not doneapplications written in this language, consisting of idempotence
carefully, the debit or credit step may be executed multiple times,(which captures the desired safety properties) and failure-freedom
leading to further correctness concerns. Services often rely on a the progress properties).
central workflow manager to manage process failures during theWe then propose language support in the form of a monad that
workflow (using distributed transactions).automatically ensures failfree idempotence. A key characteristic of
Now consider a (seemingly) different problem. Messages sentour implementation is that it is decentralized and does not require
between the client initiating the transfer and the service may be lost.distributed coordination. We show that the language support can
The only option for a client, when it does not receive a responsebe enriched with other useful constructs, such as compensations,
within some reasonable time, is to resend its request. Yet the clientwhile retaining the coordination-free decentralized nature of the
does not want the transfer to occur twice!implementation.
In this paper, we study process and communication failures inWe have implemented the idempotence monad (and its variants)
the context of workflows. The seemingly different problems causedin F# and C# and used our implementation to build realistic appli-
by process and communication failures are, in fact, inter-related.cations on Windows Azure. We find that the monad has low runtime
Idempotence, a correctness criterion that requires the system to tol-overheads and leads to more declarative applications.
erate duplicate requests, is the key to handling both communication
Categories and Subject Descriptions D.4.5 [Operating Systems]: and process failures efficiently. Idempotence, when combined with
Reliability—Fault-tolerance; C.2.4 [Computer-Communication Net- retry, gives us the essence of a workflow, a fault tolerant composi-
works]: Distributed Systems—Client/server, Distributed applica- tion of atomic actions, for free without the need for distributed co-
tions ordination. In the transfer example, a fault tolerant account trans-
fer can be implemented without a central workflow manager if the
General Terms Reliability, Languages, Design debit and credit steps can be designed to be idempotent,
Keywords fault tolerance, idempotence, workflow, transaction, Formalizing Failfree Idempotence. In this paper, we introduce a
monad simple core language , inspired by contemporary cloud plat-FAIL
forms. This formalizes process failure, duplicate requests,
1. Introduction partitioned data, and local transactions. A local transaction pro-
vides ACID guarantees but is restricted to access data within a sin-Distributed computing is becoming mainstream. Several modern
gle partition (typically a single server). Computations in areFAILplatforms offer virtualized distributed systems at low entry cost
like workflows, but without any fault-tolerance guarantees for thewith the promise of scaling out on demand. But distributed comput-
composition (i.e., the computation may fail between transactions).
We then formalize a generic correctness criterion for applica-
tions written in . A simple, powerful and tempting criterion isFAIL
that an application’s behavior in the presence of duplicate requests
Permission to make digital or hard copies of all or part of this work for personal or and process failures should be indistinguishable from its behav-
classroom use is granted without fee provided that copies are not made or distributed
ior in the absence of duplicate requests and failures. We formal-for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. To copy otherwise, to republish, to post on servers or to redistribute
1to lists, requires prior specific permission and/or a fee. In general, detecting failures perfectly in an asynchronous, message pass-
POPL’13, January 23–25, 2013, Rome, Italy. ing system is impossible [8]. Conservative failure detection can also lead to
cCopyright 2013 ACM 978-1-4503-1832-7/13/01. . . $10.00 the same problem of duplicated computation.let process (request) = workflow monad [2, 4]. We find that the core business logic in these
match requestwith applications can be declaratively expressed using the monad. Our
j (“getBalance”, (branch, account))! evaluation shows that performance overheads of using the monad
atomic branchflookupg over hand-coded implementations are statistically insignificant.
j (“transfer”, (fromBranch, fromAccount, toBranch, toAccount, amt)!
The rest of the paper is organized as follows. In Section 2, we
atomic fromBranchf
introduce a language and formalize duplicate requests andFAILupdate fromAccount ((lookup fromAccount) amt)
process failures. We formalize what it means for a applicationFAILg;
to correctly tolerate duplicate requests and failures. In Section 3,atomic toBranchf
update toAccount ((lookup toAccount) + amt) we present the idempotence monad and show how it can be used to
g; tolerate duplicate requests as well as process failures. In Section 4,
“Transfer complete.” we describe extensions of the idempotence construct. In 5,
we evaluate the idempotence monad and our implementation from
the perspective of expressiveness, benefits and overheads. Section 6Figure 1: A banking service example, in syntactically sugared
discusses related work. , that is neither idempotent nor fault-tolerant.FAIL
2. Failfree Idempotence
ize a slightly weaker, but more appropriate, correctness criterion, In this section we present a language that distils essential el-FAIL
namely failure-freedom modulo message duplication. Informally, ements of distributed computing platforms such as Windows Azure
this criterion permits the system to send duplicate responses. This and formalize the concept of failfree idempotence.
weakening is appropriate from the perspective of composition: if
the recipient of the responses can also tolerate duplicate messages, 2.1 The LanguageFAIL
then the sender is freed of the obligation to send the response ex-
Informal Overview. A programe represents a service thatFAILactly once.
receives input requests and produces output responses. An input
Automating Idempotence. Next, we address the problem of auto- requestv is processed by creating an agent to evaluateev. When
0 0matically ensuring idempotence for a service. We present our solu- the evaluation of e v terminates, producing a value v , v is sent
tion as a monad, the monad. We then show that idem- back as the response. Multiple input requests can be processed con-
potence, when coupled with a simple retry mechanism, provides a currently, and their evaluation can be interleaved. Shared, mutable,
“free” solution to the problem of tolerating process failures, guaran- persistent data is stored in tables.
teeing failure-freedom modulo message duplication. We then pro- Agents. An agent has its own internal state (captured by local
pose dedicated language support for idempotent computations. variables of the code). An agent may fail at any point in time. A
failure models problems such as hardware failure, software crashes
Decentralized Idempotence and Workflow. The idea underlying and reboots . Data stored in tables is persistent and is unaffected by
the idempotence monad is conceptually simple, but tedious to im- agent failures.
plement manually (i.e., without the monad). Given a unique iden- Tables. Tables are persistent maps. They provide primitives to
tifier associated with a computation, the monad essentially adds update the value bound to a key and lookup up the value asso-
logging and checking to each effectful step in the workflow to en- ciated with a key. The language provides a limited form of an
sure idempotance. An important characteristic of our implementa-
atomic transaction, which enables a set of operations on the same
tion (of the monad) is that it is designed to work with contemporary
table to be performed transactionally. Specifically, the construct
distributed storage systems such as key-value tables. Specifically, it
“atomic t e” evaluates e in the context of table t (lookups and
does not assume the presence of dedicated storage for logs that can
updates are permitted only on table t withine), guaranteeing iso-
be accessed atomically with each transaction. The monad reuses
lation (no other agent can accesst in the middle ofe’s evaluation)
the underlying store (in this case a key-value table) to simulate a
and the all-or-nothing property (no process failure can happen in
distinct address space for logging. the middle ofe’s evaluation).
This leads to a decentralized implementation of idempotence
that does not require any centralized storage or any (distributed) Example. Fig. 1 presents a simple bank-account-transfer exam-
coordination between different stores. Thus, the implementation ple in syntactically sugared . This example is neither idempo-FAIL
of idempotance preserves the decentralized nature of the under- tent (e.g., executing the same transfer request twice is not equiva-
lying computation. This, in turn, leads to a completely decentral- lent to executing it once) nor fault-tolerant (e.g., if the agent pro-
ized implementation of a (fault-tolerant) workflow, unlike tradi- cessing a transfer request fails in between the debit and credit
tional workflow implementations, which use a centralized work- steps).
flow coordinator and/or a centralized repository for runtime status
Syntax. Fig. 2 presents the syntax of , which extends -FAILinformation.
calculus with the primitive operations on tables explained above.
Extensions. We then extend the idempotence monad with other In the rest of the paper, we will use extensions such as natural
useful constructs, while preserving the decentralized nature of the numbers, arithmetic operators, and ordered pairs for brevity. These
construct. One extension allows the application to associate each can be encoded in the core language or added to it in the usual
transaction in a workflow with a compensating action. Another ex- fashion. We also use syntactic sugar, such as lookup e, where
tension allows the application to generate intermediate responses e62hVali, as shorthand, e.g., for ( x: lookupx)e.
to client requests and then asynchronously retry the requests on
Semantic Domains Fig. 2 defines the semantic domains used inclient’s behalf. This idiom, especially useful in long running com-
the semantics of . LethVali denote the set of all basic values:FAILputations, frees the client from having to track status of requests,
these basically consist of function abstractions. (As usual, naturaland leads to more responsive clients.
numbers, string constants, ordered pairs of values, etc. can all be
Implementation. We have implemented the idempotence work- encoded withinhVali or added to it.)
flow monad in F# targeting the Windows Azure platform. We have LethVali represent the set of optional values (of the formopt
implemented several realistic applications using the idempotence NONE or SOME v). An element of (a map fromhVali toST(a) Evaluation Contexts
::E = []jEejvE
(b) The Set of Evaluation Rules A used to define the standard semantics of .FAIL
[INPUT] [OUTPUT]
v2hVali v 2hValio
in(v) out(v ;v )i o
he; ; ;I;O i ) he; ; ]fv. (ev)g;I[fvg;Oi he; ; ]fv .vg;I;Oi ) he; ; ;I;O [f(v ;v )gii o i o
[NORMAL] [FAIL]
! 0 0h ;e i h;ei
0 0hp; ; ]fv.eg;I;Oi)hp;;]fv.eg;I;Oi hp; ; ]fv.eg;I;Oi)hp; ; ;I;O i
[ATOMIC] [UPDATE] [LOOKUP]
!
h[tn];e()i ht;vi;v2hVali
(t;k;v) !
h ; atomictnei h[tn7! t];vi ht;updatekvi ht[k7! (SOMEv)]; 0i ht;lookupkiht;t[k]i
[CONTEXT] [CONTEXT] [LIFT] [LIFT]
u [BETA]0 0 ! 00 0 0ht;eiht ;ei e!eh ;e i h;ei e!e
u ! 0 0 0 0 0 0ht;E[e]iht ;E[e ]i h ;E [e]i h;E[e ]i ht;eiht;ei h ;e i h ;e i ( x:e )v!e[v=x]
[RETRY]
v2I

he; ; ;I;O i)he; ; ]fv. (ev)g;I;Oi
(c) Additional Rules Used To Define the Ideal Semantics of .FAIL
[UNIQUE-INPUT] [DUPLINPUT] [DUPLSEND]
v2hVali;v62I v2hVali;v2I v2O
in(v) in(v) out(v)
he; ; ;I;O i ) he; ; ]fv. (ev)g;I[fvg;Oi he; ; ;I;O i ) he; ; ;I;O i he; ; ;I;O i ) he; ; ;I;O i
Figure 3: Operational semantics of .FAIL
The state of an executing program is represented by a system
x2hIdenti er i
configurationhe; ; ;I;O i2 , where e is the program itself,
v2hVali ::= x j x:e
represents the values of all tables, is the multi-set of currently
e2hExpi ::= v j e e j atomic v v j1 2 executing agents,I represents the set of all input requests received
update v v j lookup v1 2 so far, andO represents the set of all responses produced so far. (A
response to a requestv is a pair of the form (v ;v ) wherev isi i o otn2hTableNamei = hVali
the result.) Let represent the set of all configurations.
t2 = hVali7!hValiST opt Let] denote the union operator for multi-sets.
2 = hTableNamei7! T ST
hReqi = hVali
hRespi = hReqihVali Semantics. Fig. 3 presents an operational semantics for asFAIL
r(v.e)2 = hReqihExpiA a labelled transition relation) on the set of configurations . The
+ hReqi hRespi = hExpi 2 2T A evaluation of a programp starts in the initial configurationhhpii,
I Ihp; ;;;;;;i, where = t: k: NONE. (Initially, all tables map
every key to a default value ofNONE. We utilize a standard encodingFigure 2: The Syntax of and its Semantic Domains.FAIL
of optional values consisting of eitherNONE orSOMEv.)
r
System Transitions. ()) As rule INPUT indicates, the arrival of
an input requestv spawns a new agent to evaluateev. As rule OUT-
hVali ) represents the value of a single table. An element2 PUT indicates, when an agent’s evaluation completes, the resultingopt T
represents the values of all tables. value is sent back as a response. The labels on system transitions
As explained earlier, an agent represents a thread of computa- represent requests and responses. Rule NORMAL describes a nor-
tion spawned to process a given input request. The state of an agent mal system transition caused by a potentially effectful execution
is represented by a pair of the formv.e, wherev represents the step performed by a single agent, described below. As the rule in-
input request being processed ande represents a partially evaluated dicates, the execution steps of different agents can be interleaved in
expression (and represents the local state of the agent). Let rep- a non-deterministic order. Rule FAIL indicates that an agent can failA
resent the set of all agent-states. at any point in time.!
DUPLSEND. We define IDEAL to be Anf FAIL, RETRY, INPUTg[Agent Transitions. ( ) Execution steps in the evaluation of a
! f UNIQUE-INPUT, DUPLINPUT, DUPLSENDg. We refer to) asIDEALsingle agent are described by the transition relation on T
! 0 0 the ideal semantics for .FAILhExpi. A transitionh ;e i h;ei indicates that an agent expres-
0sione is transformed to an agent expressione , with the side-effect Observational Idempotence (Safety). We now consider two
0of transforming the table-state from to . The label! represents (well-studied) notions of behavioral equivalence in formalizing
a sequence of updates to a single table performed atomically in this our correctness criterion. Recall thathhpii denotes the initial con-
step. (This label, however, identifies an internal transition not visi- figuration in an execution of programp (which is the same under
ble externally, which is why the label is omitted in the correspond- both semantics). Given a labelled transition relation) on config-
ing system transition in rule NORMAL.) These transitions are of two urations, an execution of a program p (with respect to)) is an
r1types: pure (standard -calculus evaluation, BETA), and effectful, alternating sequence of states and labels, denoted ) ,0 1 n
which take the form of atomic table operations. representing a of transitions starting from the initial pro-
Atomic Table Operations. The expression “atomic t e” iden- gram state =hhpii. We say that the observed behavior obs()0
tifies a set of operations to be performed on a single table t in of an execution is the sequence of non- labels in . Note that
an atomic and failfree fashion. Its semantics is defined by rule obs() is a sequence of (input) requests and (output) responses.u
ATOMIC, which utilizes a transition relation on atomic evalua- Specifically, it does not include updates to tables, which are inter-
tion configurations of the formht;ei, which indicates the atomic nal transitions but not visible externally.
evaluation of an expressione at a table t. The labels on such tran-
DEFINITION 2.1. We say that a programp is observationallyFAILsitions are either or represent a single update to a table. Rules UP-
idempotent if for every execution ofp under the standard seman-1DATE/LOOKUP define the semantics of an update/lookup operation
tics there exists an execution ofp under the ideal semantics such2on a table. The rule ATOMIC indicates that no other execution step
that obs( ) = obs( ).1 2interleaves with the evaluation of an atomic expression. Note that
the evaluation of an atomic expression cannot fail in the middle. In We present a simpler, more abstract, formalization of idempo-
other words, either all effects of the atomic expression evaluation tence in the appendix. However, the preceding definition in terms
happen or none does. of the ideal semantics will be useful in formalizing progress prop-
Retry. The rule RETRY models one of the key ingredients used erties, as below, and in proving correctness of our implementation.
to tolerate process failures, namely a retry mechanism. The rule
Failfree Idempotence (Progress). An observationally idempotentindicates that a request must be retried periodically. Typically,
program, by definition, gives no progress guarantees. Consider aretrying logic is built into clients. A client will resend a request if it
modified version of the account-transfer example that checks thedoes not receive a response within a pre-defined amount of time.
input request to determine if it is a duplicate request and processesThis basic scheme can be optimized, as discussed in Section 4:
it only if it is not a duplicate. This ensures that the program isthe system (application) can send an acknowledgement back to the
idempotent. However, if the agent fails in between the debit andclient, after which the client can stop resending a request and the
credit steps, we would still have a problem. This motivates theapplication takes on the responsibility of retrying the request (to
following stronger correctness condition, based on the notion ofensure progress in the presence of failures). The system can exploit
weak bisimulation. A labelled transition system (S;)) consists ofvarious optimizations in implementing the retry logic, but rule

RETRY suffices for our purpose here. As we will soon see, the key a relation)SS for every‘2hLabeli.
reason for adding the RETRY rule to the semantics is to formalize
DEFINITION 2.2. A weak bisimulation between two labelled tran-a weakened progress guarantee (“progress modulo retries”) that is
sition systems ( ;) ) and ( ;) ) is a relation 1 1 2 2 1 2appropriate in the presence of failures.
such that for any we have:1 2
2.2 Formalizing Failfree Idempotence ‘ ‘0 0 00 00 0 0 01. ) ^‘ = ) 9 ; : ) ) ^ 1 1 2 21 2 2 2 2 2 1 2
We now formalize a natural correctness goal of any program: ‘ ‘FAIL 0 0 00 00 0 0 02. ) ^‘ = ) 9 ; : ) ) ^ 2 2 1 12 1 1 1 1 1 1 2namely, that it correctly handles process failures and duplicate 0 0 0 0 03. ) ) 9 : ) ^ 1 1 1 2 2 2 2 1 2messages. We will later see how we can automatically ensure this
0 0 0 0 0 0property for any program. We formalize this correctness criterion 4. ) ) 9 ; : ) ^ 2 2 2 1 1 1 1 1 1 2
as follows. We define an alternative semantics for , which weFAIL
We will write ( ; ;) ) ’ ( ; ;) ) to indicate that1 1 1 2 2 2refer to as the ideal semantics, representing an idealized execution r rthere exists a weak bisimulation between ( ;) ) and ( ;)1 21 2platform. We then define a program to be “correct” iff its behavior r) under which , where represents the set of states in 1 2 iiunder the standard semantics is equivalent to its behavior under the
that are reachable from via a sequence of) transitions. Wei iideal semantics.
will omit and in this notation if no confusion is likely.1 2
Ideal Semantics. Let A denote the set of all rules defined in
DEFINITION 2.3. A programp is said to be failfree idempo-FAILFig. 3(b). We will define the ideal semantics as a different labelled
tent iff (hhpii;) )’ (hhpii;) ).A IDEALtransition relation on program configurations, by adding and re-
moving some rules to set A. Let) denote the labelled transitionS This definition requires a failfree idempotent program to pro-
relation on induced by a given set of rulesS. Thus,) is theA vide progress guarantees: at any point in time, if the system can pro-
transition relation capturing the standard semantics of .FAIL duce a responser under the ideal semantics, then the system should
We first omit rule FAIL eliminating process failures from the be capable of producing the same response r under the standard
ideal semantics. In the ideal semantics, we assume that all input semantics also. However, the inclusion of rule RETRY in the stan-
requests are distinct, by replacing the INPUT rule by the UNIQUE- dard semantics means that this progress guarantee holds provided
INPUT and DUPLINPUT rules. We also drop rule RETRY. Finally, requests are retried. Absolute guarantees are not possible
process failures make it hard to ensure that an application sends an since an agent may fail before it executes even its first step.
output message exactly once. A common approach to this problem
THEOREM 2.4. A failfree idempotent program is also observation-is to weaken the specification and permit the application to send the
ally idempotent.same output message more than once. We do this by adding rule
663. Whenever an effectful step is executed, we simultaneously per-
sistently record the fact that this step has executed and save theletimreturn v =fun (guid, tc)! (tc, v)
value produced by this step.
letimatomic T f = 4. Every effectful step is modified to first check if this step has
fun (guid, tc)!
already been executed. If it has, then the previously saved value
atomic Tf
(for this step) is used instead of executing the step again.let key = (0, (guid, tc))in
match lookup keywith
Note that does not have any non-deterministic constructFAILj Some(v)! (v,tc+1)
(in a single agent’s evaluation). Non-deterministic constructs canj None!
be supported by treating them as an effectful step so that once alet v = f ()in (update key v); (v,tc+1)
non-deterministic choice is made, any re-execution of the same stepg
makes the same choice.
letimbind (idf, f) =
Details. We now describe in detail how individual computationfun (guid, tc)!
steps can be made idempotent and how these idempotent steps canlet (ntc, v) = idf (guid, tc)in
be composed together into idempotent computation. Our solutionf v (guid, ntc)
is essentially a monad (Fig. 4).
letimrun idf x = We represent an idempotent computation as a function that takes
let (j,v) = idf x (x, 0)in v a tuple (guid;tc) as a parameter (where guid and tc represent an
identifier and a step number used to uniquely identify steps in a
letimupdate key val = update (1,key) val
computation) and returns a value along with a new step number.
letimlookup key = lookup (1,key)
We can “execute” an idempotent computation idf as shown by the
function imrun, using the function’s argument itself as the guid
value and an initial step number of 0.Figure 4: The Idempotence Monad.
The function imreturn (the monadic “return”) lifts primitive
values to idempotent computations. This transformation can be
used for any pure (side-effect-free) expressions.Failfree Idempotent Realization. Failfree idempotence is a generic
Side-effects (table operations) are permitted only inside thecorrectness property we expect of a program. More generally,FAIL
atomic construct. The function imatomic is used to make a localthe following definition combines this property with a “specifica-
transaction idempotent. Specifically, “imatomic Tf ” is an idem-mtion” (provided as another programq).FAIL
potent representation for “atomic T f”, wheref is the monadicm
DEFINITION 2.5. A programp is said to be a failfree idem- form off constructed as described later. As explained above, thisFAIL
potent realization ofq iff (hhpii;) )’ (hhqii;) ). is represented as a function that takes a pair (guid;tc) as a param-A IDEAL
eter and realizes the memoization strategy described above. The
pair (guid;tc) is used as a unique identifier for this step. We check3. Realizing Failfree Idempotence
whether this step has already executed. If so, we return the pre-
We now present a generic, application-independent, strategy that viously computed value. If not, we execute this computation step
can be used to ensure failfree idempotence. Informally, a function and memoize the computed value. In either case, the step number
is idempotent if multiple evaluations of the function on the same is incremented in this process and returned.
argument, potentially concurrently, behave the same as a single It is, however, critical to do all of the above steps atomically
evaluation of that function with the same argument. Consider the to ensure that even if two agents concurrently attempt to execute
example in Fig. 1. In this example, the parameter requestId serves the same computation, only one of them will actually execute
to distinguish between different transfer requests (and identify du- it. However, note that an atomic expression is allowed to access
plicate requests). This service can be made idempotent and failfree only a single table. Hence, the “memoized” information for this
by (a) using this identifier to log debit and credit operations, when- computation step must be stored in the same table that is accessed
ever the operations are performed, and (b) modifying the debit and by the computation step. However, we must keep our memoization
credit steps to check, using the log, if the steps have already been and book-keeping information logically distinct from the program’s
performed. This strategy can ensure that multiple (potentially par- own data stored in the same table. We achieve this by creating two
tial and concurrent) invocations of transfer with the same identifier distinct “address spaces” (of key values) for the table. We convert
have the same effect as a single invocation. a key value k used by our idempotence implementation to (0;k)
Manually ensuring idempotence is tedious and it introduces the and convert a key value k used by the program itself to (1;k).
possibility of various subtle bugs and in general makes implementa- The functions imupdate and imlookup do this wrapping for the
tion less comprehensible. We now describe a monad-based library user’s code. Thus, the expressionf to be evaluated in the atomic
that realizes idempotence and failure-freedom in a generic way. transaction is transformed to its monadic representation f bym
replacing lookup and update inf by imlookup and imupdate
3.1 The Idempotence Monad
respectively.
The Intuition. A computation performed by a single agent con- We now consider how to compose individual computation steps
sists of a sequence of steps, “pure” as well as “effectful” ones in an idempotent computation (the monadic “bind” function). Con-
(namely, atomic local transactions which can read/update a single sider a computation of the form “let x = step1 in step2”
table.) We use the following strategy to make a computation idem- which is equivalent to “( x:step 2)step1”. We transformstep1 to
potent: its monadic form, say idf. We transform step2 to its idempotent
form, sayg. The function bind, applied to idf and x:g , produces
1. Associate every computation instance (that we wish to make the idempotent form of the whole computation. (A formal and more
idempotent) with a unique identifier. complete description of the transformation is presented later.)
2. Associate every step in an idempotent computation with a The result of “imbind idf f” is defined as follows: it is an
unique number. idempotent function that takes a parameter (guid;tc), and invokesidf (the first step). It uses the value and the step number returned by PROOF SKETCH. Let be an operationally idempotent execution
the idempotent function and invoke the second idempotent function of a program p under the standard semantics) . We show howA
0f. Thus the monad effectively threads the step number through the to construct an execution ofp under the) semantics suchIDEAL
0computation, incrementing it in every atomic transaction. that obs() = obs( ).
Note that a key characteristic of this implementation is that it is We first omit any transitions in due to the FAIL rule since their
completely decentralized. When a transaction completes, the cur- labels are empty.
rent agent simply attempts to execute the next (idempotent) transac- We next omit the transitions corresponding to repeated execution-
tion in the workflow; no coordination with a centralized transaction steps:
!manager is required. In general, distributed coordination requires The key point to note here is that an execution-step a 99K b
the use of expensive blocking protocols such as 2 phase commit. In affects the (legality of) subsequent transitions in two ways: indi-
contrast, a workflow implementation based on this idea of idempo- rectly through the side-effects! on the tables and directly through
tence coupled with (client-side) retry logic are non-blocking. The b (which may take part in subsequent transitions). A repeated
implementation does not have a single point-of-failure or single execution-step is redundant in any idempotent execution that has no
performance bottleneck, which can lead to increased scalability. failures (transitions due to the FAIL rule): it has no side-effects on
Also note that this implementation creates one log entry per the tables, and if the valueb is subsequently used in a non-repeated
transaction. Once logging for idempotence is separated from the execution-step, then we can show that another agent identical tob
core business logic, it can be optimized in several ways. We can already exists in the configuration.
avoid redundant logging if the underlying storage engine maintains We then omit any transition due to the RETRY rule. We finally
its own log. Logging can be avoided if the transaction is (declared replace INPUT transitions corresponding to a duplicate and replace
to be) semantically idempotent. INPUT transitions corresponding to a non-duplicate input request by
a UNIQUE-INPUT transition.Example. The monadic library lets us construct the monadic ver-
This leaves us with duplicate responses that may be producedsione of any expressione, by using the monadic versionm FAIL
by the OUTPUT rule for the same input (due to multiple agentsof any primitive and the monadic bind in place of function appli-
that process it). We replace these transitions by correspondingcation. E.g., the monadic version of the following code fragment
DUPLSEND transition.(from the money transfer example) 0This transformation produces an execution of p under the
0atomic fbfupdate fa ((lookup fa) amt)g; ) semantics such that obs() = obs( ).IDEAL tbf ta (( ta) + amt)g;
Our next goal is to show that all executions of programs written
is the following: using the idempotence monad are operationally idempotent. How-
ever, this claim requires the programs to be well-typed, as definedimbind
below.(imatomic fbfimupdate fa ((imlookup fa) amt)g)
f tbf ta (( ta) + amt)gg
Well-Typed IM Programs. The idempotence monad can be usedwherefeg is shorthand for x:e , wherex is not free ine.
to write monadic programs in the usual way. The monad may be
thought of as defining a new language , obtained from 3.2 Idempotence Monad Programs Are Failfree IM FAIL
by replacing the keywords atomic, lookup, and update by the
In this section, we show that programs written using the idempo-
keywords imatomic, imlookup, imupdate, imbind, and imrun.
tence monad are failfree.
A program can also be thought as a program, using theIM FAIL
definition of the monad in Fig. 4.Idempotent Executions. Consider any execution of a pro-FAIL
We first mention a few type restrictions used to simplify presen-gram. We refer to any transition generated by rule NORMAL as an
! 0 tation. We refer to-calculus terms as pure and their types as pureexecution-step and identify it by the triple (v.e) 99K (v.e ).
! types. We assume that the types of keys and values of all tables are
Thus, an execution-stepa99K b represents a transition caused by pure types. We assume that the types of the input request and the
an agent a that transforms to an agent b, with a side-effect ! on output response are also pure types.!
the tables. An execution-stepa99K b, after an execution, is said We useh ;i to denote the type of a table with keys of typek v
to be a repeated ex if the execution contains some and values of type . We assume that table names come fromk v
0! 0 some fixed set of identifiers and that the typing environment mapsexecution-step of the forma99K b . (Note that this does not sig-
these table names to their types.nify a cycle in the execution since the states of the tables could be
The non-pure terms can be classified into two kinds. The firstdifferent in the two corresponding configurations.)
kind are expressions (such as imupdatekv), which are meant to
DEFINITION 3.1. An execution is said to be operationally idempo- be evaluated in the context of a single table (as part of a local trans-
0! !0 0 action). Fig. 5 presents typing rules for intra-transaction expres-tent iff for any two execution-stepsa99K b anda 99K b in the
sions. The type!h ;i signifies a term that can be evaluated in0 0 0 vkexecution (in that order), a = a implies that b = b and ! is
the context of a table of typeh ;i, producing a value of typek vempty.
. The second kind of expressions are the ones that use the idem-
potence monad, used to represent workflow computations whichNote that operational idempotence is a property that involves the
execute one or more local transactions. Fig. 6 presents typing rulesside-effects on the tables, unlike observational idempotence. As we
for such expressions (which are the standard monad typing rules).show below, it is a stronger property that can be used to establish
In the sequel, we will use the term well-typed IM program toobservational idempotence.
refer to any expressione such that j=e : ! , wheretn i ID o i
LEMMA 3.2. Any operationally idempotent execution of a pro- and are, respectively, the types of input and output messages, ando
gramp (in the standard semantics) is observationally equivalent to provides the typings of tables. This is essentialy a program oftn
0 0 0some ideal execution ofp (in the ideal semantics): i.e., obs() = the formimrune , wheree is constructed from the other monadic
0obs( ). constructs.[IMLOOKUP] [IMUPDATE] [AT-VAR]
j= e : !h ;i j= e : !h ;i j= e : !h ;ik k v 1 k k v 2 v k v
j= imlookupe : !h ;i j= imupdatee e : unit!h ;i x :j= x : !h ;iv k v 1 2 k v k v
[AT-LAMBDA] [AT-APPLY]
h ; iv;x : j= e : !h ;i k1 2 k v j= e : ( ! )!h ;i j= e : !h ;i1 1 2 k v 2 1 k v
h ; ik v
j= x:e : ( ! !h ;i) j= e e : !h ;i1 2 k v 1 2 2 k v
Figure 5: A type system for intra-transaction expressions.
[IMATOMIC]
[IMRETURN]
h ; ik v
j=e : j=t :h ;i j= e : (unit ! )!h ;ik v k v
j= imreturne : IM j= imatomicte : IM
[IMBIND] [IMRUN]
j=e : ! IM j=e : IM j=e : ! IM2 1 2 1 1 1 2
j= imbinde e : IM j= imrune : ! 1 2 2 1 ID 2
[VAR] [LAMBDA] [APPLY]
;x : j=e : ;x : j=e :1 2 1 2
x :j=x : j= x:e : ! j= x:e : !1 2 1 2
Figure 6: A type system for idempotence monad.
p pLEMMA 3.3. All executions of a well-typed IM program are oper- define the relation’ between and byhp; ; ;I ;Oi’1 1 1 1A I
ationally idempotent. hp; ; ;I ;Oi iffI =I and = .2 2 2 2 1 2 1 2
PROOF SKETCH. Let us refer to a value of the form (0;k) (used as Note that in the above definition, the condition I = I im-1 2
a key for a table lookup/update operation) as a system key. Consider plies that both configurations have received the same set of input
any execution of a well-typed IM program. It is easy to verify that requests. The condition = implies that the processing of1 2
once the value associated with a system key (0;k) in any table is each input requestv in both configurations have gone through iden-
set to bev, it is never subsequently modified. tical sequences of effectful steps so far. (This follows since every
0! ! effectful step is memoized and is part of the table state and .)0 0 1 2Consider any two execution-stepsa99K b anda 99K b in the
0execution (in that order) wherea =a . The idempotence property THEOREM 3.6. Ifp is a well-typed IM program, then’ is a weak
p pfollows trivially whenever these steps are effect-free steps. The bisimulation between ( ;) ) and ( ;) ).A IDEALIAonly effectful steps are produced by the evaluation of animatomic
0construct. Since a = a , the key value used in the evaluation of PROOF SKETCH. Consider any ’ . The interesting transi-1 2
imatomic in both steps must be identical. The implementation tions are those that are effectful (involving an atomic operation) or
of guarantees that whatever value is produced by the produce an output. If either or can perform an interesting1 2
evaluation ofimatomic in the first step will be memoized with the transition, we must show that the other can an equivalent
given value. This guarantees that the second step will find this same transition (possibly after a sequence of silent transitions).
value in the table (thanks to the property described earlier). Hence, Consider the case when an agent v .e in can perform an1
it will evaluate to the same value and will have no side-effects on effectful transition in the standard semantics. Letv.e be the state0
the table. It follows that the execution is idempotent. of the same agent after its most recentimatomic evaluation. Then,
we must have some side-effect-free evaluatione !e e =e.0 1 k
Consider configuration . By definition, we restrict our attention2
THEOREM 3.4. Any well-typed IM program is observationally to reachable states. Hence, there exists some execution in the ideal
idempotent. semantics that produces . This execution must have received in-2
put requestv and produced an agentv. (pv). Consider the evalu-PROOF SKETCH. Follows immediately from the previous two lem-
ation of this agent. The effectful steps in this agent’s evaluation inmas.
the ideal semantics must have produced the same sequence of val-
ues as in the evaluation in the standard semantics (since the mem-As stated earlier, observational idempotence does not give us
oized values for these steps are the same in both and ). Thus,1 2any progress guarantees in the presence of failures. We now estab-
must have some agent of the formv.e for some 0 i k.2 ilish in the form of a weak bisimulation.
This will produce, after zero or more silent transitions, the agent
pDEFINITION 3.5. Letp be any program. Let denote the v.e that can then perform the same effectful transition in the idealFAIL A
set of configurationsf2 jhhpii) g that can be produced semantics as in the standard semantics.A
pby the execution ofp under the standard semantics. Let denote Consider the case when an agentv.e in can perform an ef-2I
the set of configurationsf 2 jhhpii) g that can fectful transition in the ideal semantics. We can create a new agentIDEAL
be produced by the execution of p under the ideal semantics. We v. (pv) using rule RETRY in the standard semantics. We can thenlation preserves types: translation of a well-typed programFAILV[x] = x (satisfying the restrictions mentioned above) will produced a well-
V I[ x:e ] = x: [e] typed monadic program.
I 3.4 Failfree Realization Via Idempotence[x] = imreturnx
I I[ x:e ] = ( x: [e] ) Given any expressione, we can construct its monadic versionFAIL
I I I[ne] = imbind [n] ( x: [xe] ) ,n62hVali e as explained above. The preceding results imply thate mustm m
I I I[vn] = [n] ( x: [vx] ) ,v2hVali;n62hValibe failfree. We now establish a stronger result, namely thate ism
0 I V 0 V 0 a failfree realization of e. (Failure-freedom is a weak correctness[vv ] = [v] [v ] ,v;v 2hVali
I A criterion. It indicates that a program’s behavior under the standard[atomicxe] = himatomicx [e] ;fvi
semantics is equivalent to it’s behavior under the ideal semantics.)wherefv =fxg[freevars(e)
The notion of failure-freedom does let us simplify verifying cor-
A rectness of a program by considering only its behavior under the[x] = x
A A ideal semantics. In particular, we have:[ x:e ] = x: [e]
A A A[e e ] = [e ] [e ]1 2 1 2 THEOREM 3.8. Ifp andq are weakly bisimilar under the ideal se-
A A A[updatee e ] = imupdate [e ] [e ] mantics (i.e., if (hhpii;) )’ (hhqii;) ), andp is failfree,1 2 1 2 IDEAL IDEAL
A A thenp is a failfree realization ofq.[lookupe] = imlookup [e]
PROOF SKETCH. Follows as we can compose the two weak bisim-
he;fgi = e
ulations together.
he;fxg]Yi = himbindx ( x:e );Yi
This theorem simplifies proving that a program is a failfree
Figure 7: Transforming expressions into idempotent expres- realization of another. In particular, we have already seen that aFAIL
sions. monadic program is failfree (Theorem 3.7). Hence, to prove thatem
is a failfree realization ofe, it suffices to show a weak bisimilarity
between the ideal executions of a program e and the idealFAIL
executions of its monadic representatione .duplicate the entire execution history ofv.e (which is guaranteed m
to be the same in both semantics by the definition of’). Thanks
THEOREM 3.9. Lete be the monadic representation ofe. Then,mto the idempotence property, this duplicate execution will have no
e is a failfree realization ofe.mextra side-effects and will eventually produce the same effectful
transition as in the ideal semantics. PROOF SKETCH. As explained above, it is sufficient to relate eval-
uations ofe ande under the ideal semantics. In this setting, it ism
intuitively simple to see why the monadic program “e ” simulatesm
THEOREM 3.7. A well-typed IM program is failfree. the given programe. The key distinction is that the monadic imple-
mentation uses imatomic to perform any effectful step. This step
3.3 Transforming Programs To Idempotent ProgramsFAIL will first check the memoized data to see if this step has already
We have seen that the idempotence monad lets us construct failfree executed. In an ideal execution, this check will always fail, and the
programs. Given any -programe, we can its “equiv-FAIL monadic implementation then performs the same effectful step as
alent” monadic representation using standard techniques (which are the original program (and memoizes it). The check is guaranteed
conceptually straightforward, though the details are intricate). The to always fail because the keys (g;i) used in distinct executions
transformation is presented in Fig. 7 (based on the transformation of imatomic are distinct. The value ofg will be different for exe-
in [17]). cutions corresponding to different inputsx andy. The valuei will
We make a few simplifying assumptions (type restrictions) be different for different steps corresponding to the same inputx.
about the source programe in this transformation algorithmFAIL
(similar to those mentioned in Section 3.2). We assume that the
3.5 Idempotent Failfree Computations as a Languagetypes of keys and values of all tables are pure types. We assume that
Featureintra-transaction expressions do not manipulate values of workflow
type: e.g.,atomictf x: (atomicse)g is not allowed. We have now seen how idempotent failfree computations can be
The translation is defined using multiple translation functions. automatically realized using the idempotence monad. We now pro-
V[v] is a translation function that applies only to values (which pose a new language construct for idempotent failfree computa-
Imust be of the formx or x:e ). The translation function [e] is the tions.
heart of the monadic transformation and can be applied to multi- The construct “idff v e” indicates that the computation of
transaction expressions. It uses the idempotence monad to sequence e should be failfree and should be idempotent with respect to v:
Alocal transactions. The translation function [e] is applied to intra- i.e., multiple (potentially concurrent) invocations of this construct
transaction expressions and it is used primarily to replace occur- with the same valuev behaves as though only one of the invoca-
rences ofupdate andlookup byimupdate andimlookup respec- tions executed. The above construct permits users to specify the
tively. Note that a single local transaction (i.e.intra-transaction ex- code fragment for which they desire automatic idempotence and
pression) evaluation is done using standard evaluation (without us- failure-freedom (provided by the compiler). This enables users to
ing any monad). The auxiliary functionhe;Xi is used to transform rely on other methods, perhaps application-specific, to ensure these
the monadic values used in the evaluation of multi-transactions to properties elsewhere. (For instance, some computation may be se-
standard values required in the ev of a single local transac- mantically idempotent already.) It also lets the users specify what
tion. should be used as computation identifier to detect duplicates, as
Finally, given a top-level programe (which is assumed to illustrated below.FAIL
0be a functional value of the form x:e ), it’s monadic forme is We refer to this enhanced language as . A formal seman-m IDFF
Vdefined to be imrun [e] . As usual, it can be shown that the trans- tics of appears in the appendix. We illustrate the meaning ofIDFFthe first parameter of idff using the incorrect example of Semantic Domains. The semantic domains for are theFAIL IDWF
Fig. 1. We can wrap theidff construct around this example in the same as for with minor extensions. The runtime expressionFAIL
following two ways, with different semantics. Note that the input ee is used to represent a workflow during its execution. Here,c
in this example is a pair (reqId, req) consisting of a request-id as e represents the partially evaluated form of a workflow and ec
well as the actual request. Consider: the compensating action to be performed in case the
workflow needs to be aborted. Agents can also be of the form
f =(reqId;req):idffreqId (process (reqId;req))1 idIe e , indicating an agent evaluating a workflow.w c
f =(reqId;req):idff (reqId;req) (process (reqId;req))2
Semantics. The semantics of is defined using a set of rulesIDWF
The behavior of these two functions differ in the cases where consisting of all the rules in A used to define the semantics ofFAIL
multiple inputs arrive with the same request-id but differing in the except for FAIL and ATOMIC, plus the new rules presented in Fig. 8.
second parameter req.f treats such requests as the same and will1 The initiation of a workflow (rule IDWF-BEGIN) creates a new
process only one of them, while f will treat them as different2 agent of the form id I e e , provided no agent has alreadyw c
requests and process them all. been created for id. This agent evaluates the workflow e andw
One of the subtle issues with the semantics and implementation tracks the compensating action e to be performed in case of anc
of the idff construct is the treatment of invocations that have the abort. Rule IDWF-END indicates how the computation proceeds
same id (first parameter) but have different expressions as the sec- once the workflow evaluation is complete (or if a previous work-
ond parameter. We take a simple approach with our semantics (that flow with the same id has already been initiated).
the effect is as if only the first invocation occurred). This has some The rules ATOMIC and ATOMIC-ABORT define the semantics of
implications for the underlying implementation (in the presence of transactions in a workflow. Informally, the expressionatomicte ea c
failures). One solution is to use a continuation-passing style com- is evaluated as follows. First,e is evaluated atomically to producea
putation, and memoize the entire continuation in the memoization a value v. Then, as a side-effect, the compensating action is up-
step (rather than just the value computed for the step). dated to indicate that e v should be evaluated as the first stepc
of the compensation before executing the original compensation.
Finally, the whole expression evaluates to v. Thus, note that the4. Extensions
value produced by the “atomic” actione is available to the subse-a
We have seen how idempotence can serve as the basis for fail- quent computation as well as the compensating actione . When ac
free composition of computations: essentially, a simple form of workflow is aborted (rules ATOMIC-ABORT and IDWF-ABORT), the
fault-tolerant workflow. In this section, we describe two extensions compensation expression is evaluated.
that enrich this construct, namely compensating actions and asyn- Rule ATOMIC of is replaced by the pair of rules PURE-FAIL
chronous evaluation, which simplify writing applications. These ATOMIC and PURE-ATOMIC-ABORT, which describe the behavior of
concepts are not new, but what is interesting is that they can be a transaction that is not contained within a workflow. PURE-ATOMIC
integrated without affecting the light-weight, decentralized, nature describes the successful completion of a transaction, while PURE-
of our idempotence implementation. ATOMIC-ABORT describes the case where the transaction is aborted.
(The auxiliary relation used here is defined by the rules for
4.1 Compensating Actions .)FAIL
The idff construct allows us to compose several transactions into
Compensation monad We now describe the compensation monad
an idempotent workflow that appears to execute exactly once with-
that can be used to realize workflows with compensating actions.
out process failures. However, the lack of isolation means that when
For simplicity, we describe an implementation of the compensat-
a transaction in the workflow is executed, its precondition may not
ing monad that focuses only on logical failures and compensations.
be satisfied and we may need to abort the workflow. For example,
We assume there are no duplicate requests or process failures. We
in the transfer example (Fig. 1), the debit step may succeed, but
can realize idempotent workflows with compensating actions by
we may be unable to complete the subsequent credit step because
composing this monad and the idempotence monad [13].
the account does not exist. One way of recovering from this failure
The compensation monad, shown in Fig. 9, is a combination
is to compensate for the debit by crediting the amount back to the
of the exception monad and the continuation passing style monad.
source account. If compensating actions are correct, the workflow
Transactions return a value of the form Value(v) (on successful
can guarantee all-or-nothing semantics i.e. either all or none of the
completion) or a special value Abort to indicate that the transaction
transactions in the workflow appear to execute.
was aborted. Workflows are represented as a function in continua-
We first formalize the desired semantics of workflows with com-
tion passing style. The helper function compensateWith associates
pensating actions. We present a language which providesIDWF a transaction a with a compensating action to construct a primi-
language constructs to associate transactions with compensating
tive workflow. compensateWith constructs a function in continua-
actions, and to declare logical failures. Finally, supportsIDWF tion passing style. This function first evaluatesa(). Ifa aborts, the
a construct idworkflow id e, which composes transactions with
whole transaction aborts and returns Abort. Otherwise, the contin-
compensating actions into a workflow. We present semantics of this
uation is evaluated using the value returned by the transaction. If
construct, and then show how this construct is realized using a com-
the continuation itself aborts (because one of the following trans-
pensation monad.
actions aborts), we evaluate the compensating action and return the
value Abort. The monad’s return simply lifts a value (with no com-Syntax. modifies and extends in the following waysIDWF FAIL
pensation) into a workflow. The monadic bind is standard for con-(see Fig. 8).atomicte e extends theatomic construct ofa c FAIL
tinuation passing style computations. The function run shows howby specifyinge as the compensation for the atomic transactione .c a
to execute a workflow by passing it an empty continuation.abort indicates that a logical failure has occured and the work-
flow must be aborted. idworkflowide represents an idempotent
4.2 Asynchronous evaluationworkflow with identifierid, wheree is the workflow consisting of
a composition of atomic transactions with compensations. Expres- Workflows are commonly used to perform computations involving
sion of the form ee arise only during evaluation and are not several transactions. Consequently, workflows are often long run-c
source language constructs. ning with highly variable latencies. Large latencies accentuate the(a) Syntax and Evaluation Context
x2hIdenti er i; v2hVali ::= x j x:e
e2hExpi ::= x j x:e j e e j atomicv v v j idworkflowv v j abort j update v v j lookup v j eet a c i w c
=hExpihExpi +hExpihExpiA
::E = []jEejvEjEe
(b) Evaluation Rules (in addition to Anf ATOMICg)
[IDWF-END]
[IDWF-BEGIN] idIu2 u2hVali
0 0
v.E[idworkflowidw]2 9e:idIe 2 hp; ; ]fv.E[idworkflowidw]g;I;Oi)

hp; ; ;I;O i)hp; ; ]fidI (w() 0)g;I;Oi hp; ; ]fv.E[u]g;I;Oi
[ATOMIC] [ATOMIC-ABORT]
[NORMAL]
! !! 0 0 h[tn];e ()i ht;vi;v2hVali h[tn];e ()i ht;E[abort]ia ah ;e i h;ei
! hp; ; ]fvIeg;I;Oi) h ;E [atomictne e ]ei h ;E [atomictne e ]ei a c a c
0 0
hp;;]fvIeg;I;Oi h[tn7! t];E[v] ((e v);e)i h ;E [abort]eic
[CONTEXT][IDWF-ABORT]
0e!e
0h ; (E[abort])ei h ;e i h ;E [e]ei!h ;E [e ]eic c c c
[PURE-ATOMIC] [PURE-ATOMIC-ABORT]
! !
h[tn];e ()i ht;vi;v2hVali h[tn];e ()i ht;E[abort]ia a
!
h ; atomictne ei h[tn7! t];vi h ; atomictne ei h ; 0ia c a c
Figure 8: Syntax and Semantics of .IDWF
let compensateWith a comp = queue, retrieve checkpoints, and continue evaluation, deleting the
fun f!match a()with checkpoint only when the workflow has been fully evaluated.
j Abort! Abort Supporting asynchronous evaluation requires some additional
j Value(b)!match (f b)with support from the platform and a minor change to the monad’s bind
j Abort!let = comp bin Abort
function. We assume that the platform provides a channel that can
j Value(c)! Value(c)
only be accessed by the idempotence monad (hence not exposed
in ). Messages can be sent to this channel using the functionFAILlet bind (v, f) =fun g! v (fun a! f a g)
send and received using the function recv. We assume the channellet return a = compensateWith (fun ()! a) (fun v! ())
let run a = a (fun x! Value(x)) supports the following handshake protocol for messages in order
to guarantee at-least-once processing of messages. In this protocol,
recv does not delete messages from the channel. Instead, an agent
Figure 9: The compensation monad that receives a message must acknowledge the message (using ack)
before the message is permanently deleted. If an agent crashes after
receiving a message and before acknowledging it, the message
reappears in the channel and may be processed by other agents.problem of duplicate requests because clients cannot easily distin-
(Windows Azure provides such a channel implementation, whichguish between a long running workflow and one that has failed to
our implementation uses.)generate a response. While the idempotence monad guarantees cor-
The changes to the idempotence monad are illustrated in Fig-rectness in such cases, idempotence does come at a performance
ure 10. Instead of invoking the remainder of the workflow, the mod-cost (due to log lookups). A design pattern commonly used to re-
ified bind (Fig. 10) creates a closure for the rest of the workflowduce the number of duplicate requests is for the system to take over
the task of retrying (a part of) the request on behalf of the client and persists the closure in a special queue (“worklist”) (using the
asynchronously, and sending an intermediate response to the client, function send). Special agent processes (agent) retrieve the check-
typically with the transaction identifier. The client can use transac- points (using recv) and continue evaluating the rest of workflow.
tion identifier to periodically poll for the status of the request. If an agent manages to evaluate the workflow without failing, it
The idempotence monad can be extended to support asyn- deletes the workflow from the queue (using ack). In our implemen-
chronous evaluation as follows. At a programmer defined point tation, the choice of using asynchronous evaluation (and the partic-
in the evaluation of the workflow, we create a checkpoint. A check- ular step at which to create a checkpoint) is left to the programmer.
point is essentially a closure representing the rest of the work- We evaluate the benefits of these optimizations in Section 5.
flow, along with relevant state variables. The checkpoint is then
persisted, typically in a distributed queue (essentially a worklist).
Once the checkpoint has been created, an intermediate response
is sent to the client. A set of special agents periodically query the
6

)