Towards an Automatic Proof of Lamport's Paxos

Aman Goel 0000-0003-0520-8890

University of Michigan, Ann Arbor

Karem A. Sakallah 0000-0002-5819-9089

University of Michigan, Ann Arbor

Lamport's celebrated Paxos consensus protocol is generally viewed as a complex hard-to-understand algorithm. Notwithstanding its complexity, in this paper, we take a step towards automatically proving the safety of Paxos by taking advantage of three structural features in its specification: spatial regularity in its unordered domains, temporal regularity in its totally-ordered domain, and its hierarchical composition. By carefully integrating these structural features in , a novel model checking algorithm, we were able to infer an inductive invariant that identically matches the human-written one previously derived with significant manual effort using interactive theorem proving. While various attempts have been made to verify different versions of Paxos, to the best of our knowledge, this is the first demonstration of an automatically-inferred inductive invariant for Lamport's original Paxos specification. We note that these structural features are not specific to Paxos and that can serve as an automatic general-purpose protocol verification tool.

Distributed  protocols, incremental induction, inductive invariant, invariant inference, model checking, Paxos.

§ INTRODUCTION

In this paper, we focus on proving the safety of distributed protocols like Paxos <cit.> which form the basis for implementing many efficient and highly fault-tolerant distributed services <cit.>.
Developed by Lamport, the Paxos consensus protocol allows a set of processes to communicate with each other by exchanging messages and reach agreement on a single value.
Verifying the correctness of such a concurrent system requires the derivation of a quantified inductive invariant that, together with the protocol specification, acts as an inductive proof of its safety under all possible system behaviors.

Several manual or semi-automatic verification techniques based on interactive theorem proving <cit.> have been proposed to derive a safety proof for Paxos.
Chand et al. <cit.> formally verified the TLA+ <cit.> specification of Paxos by manually deriving a proof using the TLAPS proof assistant <cit.>.
Padon et al. <cit.> used the Ivy <cit.> verifier, which requires a user to manually refine automatically-generated counterexamples-to-induction, to obtain an inductive invariant for a simplified version of Paxos in the decidable EPR fragment <cit.> of first-order logic.
The approaches in <cit.> are examples of manually-derived refinement proofs <cit.> that show how a low-level implementation refines a high-level specification.
All these methods, however, require a detailed understanding of the intricate inner workings of the protocol and entail significant manual effort to guide proof development.

In contrast, we propose an approach, implemented in the IC3PO protocol verifier, to automatically infer the required inductive invariant for an unbounded distributed protocol by adding three simple extensions to the finite-domain IC3/PDR <cit.> incremental induction algorithm for model checking <cit.>.
Symmetry boosting, introduced in <cit.>, takes advantage of a protocol's spatial regularity to automatically infer quantified strengthening assertions that reflect the protocol's structural symmetries. This paper describes range boosting and hierarchical strengthening which take advantage, respectively, of a protocol's temporal regularity and hierarchical structure, and demonstrates how IC3PO was used to automatically obtain an inductive invariant for Paxos using the four-level hierarchy shown in Figure <ref>.

Our main contributions are:

– A range boosting technique that extends incremental induction to utilize the temporal regularity in totally-ordered domains, and thus, enables automatic invariant inference for protocols with even infinite-state processes.

– A hierarchical strengthening approach to derive the required inductive invariant in a top-down step-wise procedure for hierarchically-specified distributed protocols through incremental induction extended with symmetry and range boosting, by automatically verifying high-level abstractions first and using invariants of these higher-level abstractions as strengthening assertions to derive the inductive invariant for the detailed lower-level protocol.

– Safety verification of Lamport's Paxos algorithm, both single- and multi-decree Paxos, through the derivation of a compact, human-readable inductive proof that is automatically inferred using , resulting in a drastic reduction in verification effort compared to previous approaches <cit.>.

The paper is structured as follows: <ref> presents preliminaries. <ref> and <ref> describe range boosting and hierarchical strengthening. <ref> details the four-level hierarchy we used to prove Paxos and <ref> is a record of the IC3PO run showing the actual assertions it inferred at each level of the hierarchy. <ref> discusses some of the features and interesting details on this automatically-generated proof. Experimental comparisons with other approaches are provided in <ref> and the paper  concludes with a brief survey of related work in <ref> and a discussion of future directions in <ref>.

§ PRELIMINARIES

§.§ Notation

We will use $\init, \nex$, and $\prop$ to denote the  quantified formulas that specify, respectively, a protocol's initial states, its transition relation, and the safety property that is required to hold on all reachable states.
We use primes (e.g., $\varphi'$) to represent a formula after a single transition step. The notation $\ev A$ (resp. $\eps A$, $\epa A$, and $\ep A$) means that assertion $A$ was inferred by IC3PO for the (resp. , , and ) protocol.

As an example, consider a protocol $\mathcal{P}$ with two  sorts, a symmetric sort $\fin{aSort}$ and a totally-ordered sort  $\fin{bSort}$, along with relations $p(\fin{aSort}, \fin{bSort})$ and $q(\fin{bSort})$ defined on these sorts.
Viewed as a parameterized system $\mathcal{P}(\fin{aSort}, \fin{bSort})$, we can specify its finite instance $\mathcal{P}(3, 4)$ as:

\begin{align}
\mathcal{P}(3, 4) : \hspace{20pt} &\fin{aSort_3} \triangleq \{ \fin{a_1}, \fin{a_2}, \fin{a_3} \}  \nonumber\\
&\fin{bSort_4} \triangleq [ \fin{b_{min}, b_1, b_2, b_{max}} ] \label{eq:ex_size}
\end{align}

where $\fin{aSort_3}$ represents the finite symmetric sort of this instance defined as a set of arbitrarily-named distinct constants, while the finite totally-ordered sort $\fin{bSort_4}$ is composed of a list of ordered constants, i.e., $\fin{b_{min} < b_1 < b_2 < b_{max}}$.
This instance can be encoded using twelve $p$ and four $q$ $\BOOLEAN$ state variables. A state of this instance corresponds to a complete assignment to these $16$ state variables, with a total state-space size of $2^{16}$.
We will use $\fnex$ instead of $\nex$ to denote the transition relation of the finite instance.

§.§ Clause Boosting and Quantifier Inference

The basic framework for inferring the quantified assertions required to prove protocol safety is described in <cit.>. It extends the finite IC3/PDR incremental induction algorithm by boosting its clause learning during the 1-step backward reachability checks performed through Satisfiability Modulo Theories (SMT) <cit.> solving. Specifically, a clause $\varphi$ is learned in (and refines) frame $F_i$ if the 1-step query $\psi_i := F_{i-1} \wedge \fnex \wedge [\neg \varphi']$ is unsatisfiable. This means that cube $\neg \varphi$ in frame $F_i$ is unreachable from frame $F_{i-1}$.
Boosting refers to: a) “growing” $\varphi$ to a set of clauses that also satisfy this unreachability constraint from frame $F_{i-1}$, and b) refining the frame $F_i$ with the entire clause set instead of just $\varphi$.
Such boosting accelerates the convergence of incremental induction but, more importantly, makes it possible, under some regularity assumptions, to represent this set of clauses by a single logically-equivalent quantified clause $\Phi$ and is the key to generalizing the results of such finite analysis to unbounded domains.

§.§ Symmetric Boosting and Quantifier Inference

Protocols that are strictly specified in terms of symmetric sorts can be characterized as having spatial regularity. For example, the constants in a sort representing a finite set of $k$ identical processes are essentially indistinguishable replicas that can be permuted arbitrarily without changing the protocol behavior. A learned clause $\varphi$ parameterized by the constants of such a sort can be boosted by permuting its constants in all possible $k!$ ways yielding a set of symmetrically-equivalent clauses, i.e., its symmetry orbit $\varphi^{Sym_k}$ under the full symmetric group $Sym_k$. By construction, all clauses in $\varphi$'s orbit automatically satisfy the unreachability constraint without the need to perform additional 1-step queries.
Furthermore, the quantified clause $\Phi$ that encodes $\varphi$'s orbit is algorithmically constructed by a syntactic analysis of $\varphi$'s structure, and can involve complex universal and existential quantifier alternations over both state and non-state (auxiliary) variables. The reader is referred to <cit.> for the complete details of the connection between symmetry and quantification and the procedure for quantifier inference.

§.§ Finite Convergence

When a boosted finite incremental induction run terminates, it either produces a finite counterexample demonstrating that the specified safety property fails, or produces a set of quantified assertions $A_1, \cdots, A_n$ that yield the inductive invariant $inv = Safety \wedge A_1 \wedge \cdots \wedge A_n$ proving safety for the given finite size. At this point, an algorithmic finite convergence procedure is invoked to check if the current instance size has captured all possible protocol behaviors and, if not, to systematically increase the finite instance size until protocol behavior saturates and the cutoff size is reached <cit.>.

§ RANGE BOOSTING

Clause boosting is not limited to clauses that are parameterized by the constants of symmetric sorts, and can be extended to clauses whose literals depend on the constants of totally-ordered sorts such as  ballot, round, epoch, etc., that are used to model the temporal order of events in a distributed protocol. However, the boosting procedure for such clauses differs from symmetric boosting in two ways: a) the ordering relation between totally-ordered constants must be explicitly preserved, and b) adherence of a boosted clause to the unreachability constraint is not guaranteed and must be explicitly checked with a 1-step backward reachability query.

We extended with a range boosting procedure that complements its symmetry boosting mechanism, allowing it to transparently handle protocols with both symmetric and totally-ordered sorts.

Let  $\varphi$ be a clause that is parameterized by totally-ordered constants and let $\varphi^{Ordered}$ denote those variants of $\varphi$ that are obtained by ordering-compliant permutations of its constants.

Clause $\varphi$ is boosted by making 1-step backward reachability queries on $\varphi^{Ordered}$ to identify its safe subset $\varphi^{Safe}$,  i.e., those variants that satisfy the unreachability constraint.

For example, consider the following clause $\varphi_1$ defined on the finite instance $\mathcal{P}(3,4)$ from (<ref>):

\begin{align}
\varphi_1 =&~ p(\fin{a_1, b_1}) \vee q(\fin{b_2}) \label{eq:clause1}
\end{align}

Since $\varphi_1$ contains two ordered constants $(\fin{b_1}, \fin{b_2})$, it has six ordering-compliant variants $ \fin{(b_{min},b_1)},$ $\fin{(b_{min},b_2)},$ $\fin{(b_{min},b_{max})},$ $\fin{(b_1,b_2)},$ $\fin{(b_1,b_{max})}$, and  $\fin{(b_2,b_{max})}$. However only three of these variants end up satisfying the unreachability constraint yielding the following safe subset of $\varphi_1^{Ordered}$:

\begin{align}
\varphi_1^{Safe} =&~ [~ p(\fin{a_1, b_1}) \vee q(\fin{b_2}) \hspace{8pt} ~]~ \wedge \nonumber\\
&~ [~ p(\fin{a_1, b_1}) \vee q(\fin{b_{max}}) ~]~ \wedge \nonumber\\
&~ [~ p(\fin{a_1, b_2}) \vee q(\fin{b_{max}}) ~]~ \label{eq:clause1_orbit2}
\end{align}

The inferred quantified clause that encodes these three clauses is now constructed using two universally-quantified variables $X_1, X_2 \in \fin{bSort_4}$ that replace $\fin{b_1}$ and $\fin{b_2}$ in $\varphi_1$ and expressed as an implication whose antecedent specifies a constraint over the ordered “range” $\fin{b_{min}} < X_1 < X_2$ that must be satisfied by the quantified variables:

\begin{align}
& \Phi_1 =~ \forall X_1, X_2 \in \fin{bSort_4}: \nonumber\\
& \hspace{20pt} (\fin{b_{min}} < X_1) \wedge (X_1 < X_2) \to [~ p(\fin{a_1}, X_1) \vee q(X_2) ~] \label{eq:clause1_quant2}
\end{align}

In general, a clause that is parameterized by $k$ constants from a totally-ordered domain whose size is greater than $k$ can be range-boosted and encoded by a universally-quantified predicate with $k$ variables which is expressed as an implication whose antecedent is a range constraint that evaluates to true for just those combinations of the $k$ variables that correspond to safe variants of $\varphi$.

This procedure extends easily to the case of multiple totally-ordered domains as well, allowing range boosting to be performed independently for each such domain in any order since constants from different domains do not interfere with each other.

§ HIERARCHICAL STRENGTHENING

As advocated in <cit.>, hierarchical structuring is an effective way to manage complexity during manual proof development. It can also be easily incorporated in the style of invariant generation based on symmetry and range boosting.

Given a low-level specification $L$ that implements a high-level specification $H$, i.e., $L \prec H$, hierarchical strengthening starts by automatically deriving strengthening assertions $\eh A^H $ that, together with the safety property $\eh \prop$, proves the safety of $H$. It then maps and propagates $\eh A^H$ to $L$, denoted as $\el A^H$, and proceeds to prove the strengthened property $\el \prop \wedge \el A^H$ in $L$ by deriving any additional assertions $\el A^L$ needed to establish the safety of $L$. The underlying assumption in this procedure is that proving $H$ is much easier than proving $L$ directly, and that any assertions derived to prove $H$ are also applicable, with suitable mapping, to $L$. The final inductive invariant that proves $L$ will, thus, have the form $\el inv = (\el \prop \wedge \el A^H) \wedge \el A^L$ which can be interpreted as reducing the complexity of $L$'s proof by strengthening its safety property with assertions derived for $H$.

Such strengthening can be extended to a $k$-level hierarchy $H \prec M_1 \prec \cdots \prec M_{k-2} \prec L$, where $M_1$ to $M_{k-2}$ are suitably-defined intermediate levels between $H$ and $L$.
This, in turn, allows single-level automatic verification techniques based on incremental induction, like , to scale to complex protocols like , by step-wise verifying higher-level abstractions first and using their auto-generated proofs to incrementally build the proof for the lower-level protocol.

§ HIERARCHICAL SPECIFICATION OF PAXOS

This section describes in detail the multi-level hierarchical structure of the Paxos protocol, as shown earlier in Figure <ref>.

§ HIERARCHICAL VERIFICATION OF PAXOS

Using the 4-level hierarchy $\paxos \prec \paxosabstract \prec \paxossimple \prec \voting$, this section is a “log” of how IC3PO automatically derived the required strengthening assertions that established the safety of Paxos.

§.§ Proving

Using instance $\voting(2,3,3,4)$, proved the safety of by automatically deriving the inductive invariant $\ev inv \triangleq \ev Safety \wedge \ev A_1 \wedge \ev A_2$ where

\begin{align}
% & \ev Inv_{\voting} =~ \ev \prop \wedge \ev A_1 \wedge \ev A_2 \label{eq:inv_voting}\\
& \ev A_1 =~ \forall A \in \sacceptor, B \in \sballot, V \in \svalue : \nonumber\\
& \hspace{40pt} votes(A, B, V) \to isSafeAt(B, V) \nonumber\\
& \ev A_2 =~ \forall A \in \sacceptor, B \in \sballot, V_1, V_2 \in \svalue : \nonumber\\
& \hspace{37pt} chosenAt(B, V_1) \wedge votes(A, B, V_2) \to (V_1 = V_2) \nonumber
\end{align}

In words, these two strengthening assertions mean:

$A_1$: If an acceptor voted for value $V$ in ballot number $B$, then $V$ is safe at $B$.

$A_2$: If value $V_1$ is chosen at ballot $B$, then no acceptor can vote for a value different than $V_1$ in $B$.

§.§ Proving

Using the refinement mapping $[votes \leftarrow msg2b$, $maxBal \leftarrow maxBal]$, transformed $\ev A_1$ and $\ev A_2$ to the following corresponding versions for :

\begin{align}
& \eps A_1 =~ \forall A \in \sacceptor, B \in \sballot, V \in \svalue : \nonumber\\
& \hspace{40pt} msg2b(A, B, V) \to isSafeAt(B, V) \nonumber\\
& \eps A_2 =~ \forall A \in \sacceptor, B \in \sballot, V_1, V_2 \in \svalue : \nonumber\\
& \hspace{40pt} chosenAt(B, V_1) \wedge msg2b(A, B, V_2) \to (V_1 = V_2) \nonumber
\end{align}

These two assertions, passed down from the proof of , represented a strengthening of the safety property of that allowed to prove it with the inductive  invariant $\eps inv \triangleq \eps Safety \wedge \mathop  \bigwedge \nolimits_{1 \le i \le 6} \eps A_i$ where

\begin{align}
& \eps A_3 =~ \forall B \in \sballot, V \in \svalue : \nonumber\\
& \hspace{50pt} msg2a(B, V) \to isSafeAt(B, V) \nonumber\\
& \eps A_4 =~ \forall B \in \sballot, V_1, V_2 \in \svalue : \nonumber\\
& \hspace{50pt} msg2a(B, V_1) \wedge msg2a(B, V_2) \to (V_1 = V_2) \nonumber\\
& \eps A_5 =~ \forall A \in \sacceptor, B \in \sballot, V \in \svalue : \nonumber\\
& \hspace{50pt} msg2b(A, B, V) \to msg2a(B, V) \nonumber\\
& \eps A_6 =~ \forall A \in \sacceptor, B \in \sballot : \nonumber\\
& \hspace{50pt} msg1b(A, B) \to maxBal(A) \geq B \nonumber
\end{align}

are four additional automatically-generated strengthening assertions that express the following facts about :

$A_3$: If ballot $B$ leader sends a $2a$ message for value $V$, then $V$ is safe at $B$.

$A_4$: A ballot leader can send $2a$ messages only for a unique value.

$A_5$: If an acceptor voted for a value in ballot number $B$, then there is a $2a$ message for that value at $B$.

$A_6$: If an acceptor has sent a $1b$ message at a ballot number $B$, then its $maxBal$ is at least as high as $B$.

§.§ Proving

All variables from refine to as is, except for $msg1b$ that adds explicit tracking of the maximum vote voted by an acceptor in .
Assertions $\eps A_1$ to $\eps A_5$ map to $\epa A_1$ to $\epa A_5$ in as is, while $\eps A_6$ maps as:

\begin{align}
& \epa A_6 =~ \forall A \in \sacceptor, B, B_{max} \in \sballot, V_{max} \in \svalue : \nonumber\\
& \hspace{50pt} msg1b(A, B, B_{max}, V_{max}) \to maxBal(A) \geq B \nonumber
\end{align}

These six assertions, passed down from the proof of , represented a strengthening of the safety property of that allowed to prove it with the inductive  invariant $\epa inv \triangleq \epa Safety \wedge \mathop  \bigwedge \nolimits_{1 \le i \le 8} \epa A_i$ where

\begin{align}
% & \epa Inv =~ \epa \prop_{strong2} \wedge \epa A_7 \wedge \epa A_8  \label{eq:inv_paxos_abstract}\\
& \epa A_7 =~ \forall A \in \sacceptor, B, B_{max} \in \sballot, V_{max} \in \svalue : \nonumber\\
& \hspace{16pt} [(B > -1) \wedge (B_{max} > -1) \wedge msg1b(A, B, B_{max}, V_{max})] \nonumber\\
& \hspace{115pt} \to msg2b(A, B_{max}, V_{max}) \nonumber\\
& \epa A_8 = \forall A \in \sacceptor, B, B_{mid}, B_{max} \in \sballot, \nonumber\\
& \hspace{37pt} V, V_{max} \in \svalue : \nonumber\\
& \hspace{10pt} [(B > B_{mid}) \wedge (B_{mid} > B_{max}) \wedge msg1b(A, B, B_{max}, V_{max})] \nonumber\\
& \hspace{115pt} \to \neg msg2b(A, B_{mid}, V) \nonumber
\end{align}

are two additional automatically-generated strengthening assertions that express the following facts about :

$A_7$: If an acceptor issued a $1b$ message at ballot number $B$ with the maximum vote $\langle B_{max}, V_{max} \rangle$, and both $B$ and $B_{max}$ are higher than $-1$, then  the acceptor has voted for value $V_{max}$ in ballot $B_{max}$.

$A_8$: If an acceptor issued a $1b$ message at ballot number $B$ with the maximum vote $\langle B_{max}, V_{max} \rangle$, then  the acceptor cannot have voted in any ballot number strictly between $B_{max}$ and $B$.

§.§ Proving

All variables from refine to trivially, mapping $\epa A_1,\dots,\epa A_8$ to $\ep A_1,\dots,\ep A_6$ in as is.
These eight assertions, passed down from the proof of , represented a strengthening of the safety property of that allowed to prove it with the inductive  invariant $\ep inv \triangleq \ep Safety \wedge \mathop  \bigwedge \nolimits_{1 \le i \le 11} \ep A_i$ where

\begin{align}
% & \ep Inv =~ \ep \prop_{strong3} \wedge \ep A_9 \wedge \ep A_{10} \wedge \ep A_{11} \label{eq:inv_paxos}\\
& \ep A_9 =~ \forall A \in \sacceptor : maxVBal(A) \leq maxBal(A) \nonumber\\
& \ep A_{10} =~ \forall A \in \sacceptor, B \in \sballot, V \in \svalue : \nonumber\\
& \hspace{60pt} msg2b(A, B, V) \to maxVBal(A) \geq B \nonumber\\
& \ep A_{11} =~ \forall A \in \sacceptor : maxVBal(A) > -1 \nonumber\\
& \hspace{60pt} \to msg2b(A, maxVBal(A), maxVal(A)) \nonumber
\end{align}

are three additional automatically-generated strengthening assertions that express the following facts about :

$A_9$: $maxVBal$ of an acceptor is less than or equal to its $maxBal$.

$A_{10}$: If an acceptor voted in a ballot number $B$, then its $maxVBal$ is at least as high as $B$.

$A_{11}$: If acceptor $A$ has its $maxVBal$ higher than $-1$, then $A$ has already cast a vote $\langle maxVBal(A), maxVal(A)\rangle$.

§ DISCUSSION

This section provides a discussion about certain key points and features about the proof from Section <ref>.

§.§ Comparison against Human-written Invariants

Optionally, the inductive invariant $\ep inv$ can be minimized to derive a subsumption-free and closed set of invariants, which removes $A_1$ and $A_2$ that are subsumed by the conjunction $A_3 \wedge A_4 \wedge A_5$.
After this minimization, the inductive invariant of matches identically with the manually-written and TLAPS-checked inductive invariant from <cit.>, guaranteeing its correctness.
Similarly, the inductive invariant of , i.e., $\ev inv$, matches directly with the manually-written and TLAPS-checked inductive invariant from <cit.>.

§.§ Benefits of Range Boosting

Assertions $A_6$ to $A_{11}$ express conditions defined over ordered ranges in the infinite totally-ordered $\sballot$ domain. Inferring such invariants automatically through becomes possible through range boosting (Section <ref>), that extends incremental induction with the knowledge of temporal regularity over totally-ordered domains by learning quantified clauses over ordered ranges.

§.§ Protocol's Formula Structure

Note that $A_1$ to $A_3$ use definitions $isSafeAt$ and $chosenAt$, which implicitly enables to incorporate learning with complex quantifier alternations. Inspired from previous works on the importance of using derived/ghost variables <cit.>, utilizes the formula structure of the protocol's transition relation in a unique manner, by incorporating definitions in the protocol specification as auxiliary non-state variables during reachability analysis, described in detail in <cit.>. This provides a simple and inexpensive procedure to incorporate clause learning with complex quantifier alternations.

§.§ Decidability

Protocol specifications at each of the four levels include quantifier alternation cycles that make unbounded SMT reasoning fall into the undecidable fragment of first-order logic.

Unsurprisingly, previous works that rely on unbounded SMT reasoning, like SWISS <cit.>, fol-ic3 <cit.>, DistAI <cit.>, I4 <cit.>, and UPDR <cit.>, struggle with verifying Lamport's Paxos. , on the other hand, performs incremental induction and finite convergence over finite protocol instances using finite-domain reasoning that is always decidable.

§.§ Why a Four-Level Hierarchy?

The original Paxos specification is composed of a two-level hierarchy $\paxos \prec \voting$.

Given the two strengthening assertions $A_1$ and $A_2$ from , inferring the remaining nine assertions for directly in one step of hierarchical strengthening is difficult, since these two specifications are too far apart to be proved directly. struggled with the large state space of and learnt too many weak clauses involving $msg1b$, $maxVBal$ and $maxVal$, eventually running out of memory due to invariant inference getting confused with several counterexamples-to-induction.
Table <ref> compares the state-space size of protocol instances at each of the four hierarchical levels.
Even though $2^{147}$ is not huge, especially with respect to hardware verification problems <cit.>, has a dense state-transition graph where state-transitions are tightly coupled with high in- and out- degree, making the problem difficult for automatic invariant inference with incremental induction based model checking.

1c|Finite Instance     State-space Size

$\voting(2,3,3,4)$     $2^{30}$

$\paxossimple(2,3,3,4)$     $2^{54}$

$\paxosabstract(2,3,3,4)$     $2^{138}$

$\paxos(2,3,3,4)$     $2^{147}$

State-space size for finite instances with 2 $\fin{value}$, 3 $\fin{acceptor}$, 3 $\fin{quorum}$, and 4 $\fin{ballot}$

Adding reduced the complexity in by abstracting away $maxVBal$ and $maxVal$.
Still, scalability remained a challenge due to $msg1b$, that contributed to 96 out of 147 state bits in $\paxos(2,3,3,4)$.
Adding another level, i.e., $\paxossimple$, removed 84 out of these 96 state bits by abstracting away explicit tracking of the maximum vote of an acceptor from $msg1b$.
When compared against $\paxos$, $\paxossimple$ is significantly simpler, with a total state-space size to be just $2^{54}$ for its finite instance $\paxossimple(2,3,3,4)$, which led to successfully prove automatically using the four-level hierarchy.

§.§ Extension to and

Till now, by we meant single-decree Paxos which is the core consensus algorithm underlying the complete Paxos state-machine replication protocol <cit.>, commonly referred to as  <cit.>. In , a sequence of instances execute single-decree such that the value chosen in the $i^{th}$ instance becomes the $i^{th}$ command executed by the replicated state machine. Additionally, if the leader is relatively stable, $Phase1$ becomes unnecessary and is skipped, reducing the failure-free message delay from 4 delays to 2 delays.

Mapping each of the assertions $A_1,\dots,A_{11}$ to is trivial, and simply adds the corresponding instance as an additional universally-quantified argument, e.g., $A_{11}$ maps as:

\begin{align}
& \emp A_{11} = \forall A \in \sacceptor, I \in \sinstance : \nonumber\\
& \hspace{50pt} maxVBal(A, I) > -1 \nonumber\\
& \hspace{50pt} \to msg2b(A, I, maxVBal(A, I), maxVal(A, I)) \nonumber
\end{align}

Unsurprisingly, the 11 strengthening assertions, passed down from the proof of , together with the safety property of , allowed to trivially prove it with no additional strengthening assertions needed, meaning $\emp \prop \wedge \mathop  \bigwedge \nolimits_{1 \le i \le 11} \emp A_i$ is already an inductive invariant of . As described in previous works <cit.>, the crux of proving the safety of is based on proving single-decree since each consensus instance participates independently without any interference from other instances. Our experiments validated this further.

Similarly, we also tried another Paxos variant called  <cit.>, which also verifies trivially with the same inductive invariant, i.e., with no additional strengthening assertions needed.

§ EXPERIMENTS

<cit.> currently accepts protocol descriptions in the Ivy language <cit.> and uses the Ivy compiler to extract a logical formulation of the protocol in a SMT-LIB <cit.> compatible format.
To get an idea on the effectiveness of hierarchical strengthening, we also evaluated automatically deriving inductive proofs for EPR variants of Paxos from <cit.> without any hierarchical strengthening. These specifications describe Paxos in the EPR fragment <cit.> of first-order logic and also incorporate simplifications equivalent to the ones described for in Section <ref>.
We performed a detailed comparison against other state-of-the-art techniques for automatically verifying distributed protocols:

–  <cit.> uses SMT solving to derive an inductive invariant by performing an enumerative search in an optimized and bounded invariant search space.

–  <cit.>, implemented in mypyvy <cit.>, extends IC3 with a separators-based technique that performs enumerative search for a quantified separator in the space of bounded mixed quantifier prefixes.

–  <cit.> performs data-driven invariant learning by enumerating over possible invariants derived from simulating a protocol at different instance sizes, followed by iteratively refining and checking candidate invariants.

–  <cit.> performs finite-domain IC3 (without accounting for regularity) using the AVR model checker <cit.>, followed by iteratively generalizing and checking the inductive invariant produced by AVR.

– , from the mypyvy <cit.> framework, implements PDR$^{\forall}$/UPDR <cit.> for verifying distributed protocols.

All experiments were performed on an Intel (R) Xeon CPU (X5670). For each run, we used a 5-hour timeout and a 32 GB memory limit. All tools were executed in their respective default configurations. We used Z3 <cit.> version 4.8.10, Yices 2 <cit.> version 2.6.2, and CVC4 <cit.> version 1.8.

§.§ Results

Table <ref> summarizes the experimental results. variants were run without any hierarchical strengthening. For problems, we employed hierarchical strengthening using each tool to verify Lamport's original Paxos specification (and its variants) through higher-level strengthening assertions that were automatically generated from (as detailed in Section <ref>). Note that problems include quantifier-alternation cycles that make unbounded SMT reasoning fall into the undecidable fragment of first-order logic.

emerges as the only successful technique that verifies Lamport's Paxos and its variants, and automatically infers the required inductive invariants efficiently. Unsurprisingly, none of the other tools (i.e., , , , and ) were able to solve problems since each of these tools rely on unbounded SMT reasoning and struggle on problems that fall outside the decidable EPR fragment of first-order logic.

§.§ Discussion

§.§.§ Effect of hierarchical strengthening

Comparing versus shows the advantages offered by hierarchical strengthening.
Even though was able to automatically verify EPR versions of single-decree Paxos and flexible Paxos from <cit.>, none of the tools were able to automatically verify the EPR version of multi-decree Paxos. variants, on the other hand, employed hierarchical strengthening which allowed to verify Lamport's Paxos automatically and efficiently by using the protocol's hierarchical structure.

§.§.§ Comparison against other verifiers

failed on all problems due to unsupported constructs and parsing errors.
and (as well as ) are limited to generating only universally-quantified invariants over state variables, and hence, were unable to solve any problem.
While both and use incremental induction over a finite protocol instance, the number of SMT queries made by grows drastically, indicating the benefits offered by symmetry and range boosting employed in .
also fails on all problems, showing limited scalability of its enumeration-based separators technique operating directly in the unbounded domain. For , we weren't able to replicate results for problems as reported in <cit.> using our experimental setup. Nevertheless, showed limited capabilities for solving problems.

§.§.§ Comparison against human-written invariants

As evident from $A_1$ to $A_{11}$ in Section <ref>, generated concise, human-readable inductive invariants. In fact, every invariant of written manually by Lamport et al. (as detailed in <cit.>) had a corresponding equivalent invariant in the inductive proof automatically generated with . In contrast, deriving such invariants manually, even in the presence of a hierarchical structure, is a tedious and error-prone process that demands deep domain expertise <cit.>.

Overall, the evaluation confirms our main hypothesis, that it is possible to utilize the regularity and hierarchical structure in complex distributed protocols, like in Paxos, to scale automatic verification beyond the current state-of-the-art.

§ RELATED WORK

Introduced by Lamport, TLA+ is a widely-adopted language for the specification and verification of distributed protocols <cit.>. The TLA+ toolbox <cit.> provides the TLC model checker, which is primarily used as a debugging tool for verifying small finite protocol instances <cit.>, and not as a tool for inferring inductive invariants. The TLAPS proof assistant <cit.> allows checking proofs manually written in TLA+, and has been used to verify several distributed protocols, including variants of Paxos <cit.>.

The derivation of inductive invariants for distributed protocols continues to be mostly carried out through refinement proofs using interactive theorem proving <cit.>, which demands significant manual effort and profound domain expertise.
The first attempts at automatically deriving quantified invariants were reported in <cit.>, using invisible invariants.
The intuition underlying this method was the assumption that the system is “sufficiently symmetric,” and that its behavior can be captured by any $m$-subset of its processes as a universally-quantified invariant. However, universally-quantified invariants are not guaranteed to be inductive or to imply the safety property. Spatial regularity was further explored in <cit.> to reduce the verification of an $n$-process system to that of a quotient system at a small cutoff size.

Notwithstanding the undecidability result of Apt and Kozen <cit.>, many efforts to automatically infer quantified inductive invariants have been reported with the pace increasing in recent years <cit.>.
Verification of parameterized systems is further explored in <cit.>.
However, unlike , these methods generally do not scale to complex protocols like Lamport's Paxos, since these methods rely heavily on unbounded reasoning and are limited to specifications in the EPR fragment of first-order logic.

Our technique builds on these works, with the capability to automatically infer the required quantified inductive invariant using the latest advancements in model checking, by extending our recent work <cit.> on symmetry boosting and finite convergence with range boosting and hierarchical strengthening.

§ CONCLUSIONS & FUTURE WORK

We proposed range boosting, a novel technique that extends the incremental induction algorithm to utilize the temporal regularity in distributed protocols through quantified reasoning over ordered ranges.
We also presented hierarchical strengthening, a simple technique that utilizes the hierarchical structure of protocol specifications to enable automatic verification of complex distributed protocols with high scalability.

Given the four-level hierarchy of the Paxos specification, we showed that these techniques, coupled with our recent work on symmetry boosting and finite convergence, provide, to our knowledge, the first demonstration of an automatically-inferred inductive invariant for the original Lamport's Paxos algorithm.

While introducing and to get the four-level Paxos hierarchy was quite easy, these intermediate levels were still added manually.
It is appealing to explore counterexample-guided abstraction-refinement (CEGAR) techniques <cit.>
to automatically identify these intermediate levels whenever needed to overcome complexity.
Specifically, investigating how to leverage clause learning feedback from incomplete runs to identify bottlenecks in proof inference and utilizing this information to automatically abstract away irrelevant details from the low-level protocol can help in making the complete procedure automatic end-to-end.
We leave this investigation as future work.

Exploring inference with existential quantifiers in range boosting can also be an interesting future direction, though intuitively, existential quantification over temporal behaviors looks unnecessary for proving safety properties.
Future work also includes automatically inferring inductive proofs for other distributed protocols, such as Byzantine Paxos <cit.>, Raft <cit.>, etc., and exploring the verification of consensus algorithms in blockchain applications.

§ DATA AVAILABILITY STATEMENT AND ACKNOWLEDGMENTS

tocsectionData Availability Statement and Acknowledgments
The software and data sets generated and analyzed during the current study, including all experimental data, evaluation scripts, and source code are available at <https://github.com/aman-goel/fmcad2021exp>.

We thank Leslie Lamport for the TLA+ video course <cit.>, which shaped several ideas presented in this paper. We thank the developers of TLA+ <cit.>, Yices <cit.>, Z3 <cit.>, pySMT <cit.>, and Ivy <cit.> for making their tools openly available.
We also thank the reviewers for their valuable comments.

§ APPENDICES

We include additional/supplementary material in the appendices, as follows:

Appendix <ref>: Finite instance sizes used in the experiments

– Lists down the instance sizes for and for each protocol in the evaluation (Section <ref>)

Appendix <ref>: TLA+ description for and

– Presents full TLA+ descriptions of and


ad short = AD, long = automatic differentiation cbpv short = CBPV, long =
call-by-push-value

# Automatic Differentiation via Effects and Handlers

An Implementation in Frank

Jesse Sigal  0000-0002-5117-8752 University of EdinburghEdinburghU.K.
<EMAIL_ADDRESS>
###### Abstract.

ad is an important family of algorithms which enables derivative based
optimization. We show that ad can be simply implemented with effects and
handlers by doing so in the Frank language. By considering how our
implementation behaves in Frank’s operational semantics, we show how our code
performs the dynamic creation of programs during evaluation.

automatic differentiation, algebraic effects, effect handlers, differentiable
programming

††copyright: none††conference: Partial Evaluation and Program Manipulation;
January 18–19; Online††ccs: Theory of computation Operational semantics††ccs:
Theory of computation Control primitives††ccs: Mathematics of computing
Automatic differentiation

##  1\. Introduction

Machine learning, artificial intelligence, scientific modelling, information
analysis, and other data heavy fields have driven the demand for tools which
enable derivative based optimization. The family of algorithms known as ad is
the foundation of the tools which achieve this. The family can be coarsely
divided into forward mode and reverse mode. Multiple modes exist because their
asymptotics depend on different features of the differentiated programs.
Forward mode ad was introduced in 1964 by Wengert (Wengert, 1964), and reverse
mode ad was created by Speelpenning in his 1980 thesis (Speelpenning, 1980).

It is not surprising that, given its history, ad has been implemented in many
different ways. Many popular tools such as ADIFOR (Bischof et al., 1996), ADIC
(Bischof et al., 1997), and Tapenade (Pascual and Hascoët, 2008; Hascoët and
Pascual, 2013) work via source transformation. These transformations take
place on languages such as C and FORTRAN, and thus all of the aforementioned
tools work externally from the program being written. We shall show here that
the recent Frank language (Lindley et al., 2017; Convent et al., 2020) and its
operational semantics, which leverages effects and handlers, can be informally
seen as dynamically performing partial evaluation and program manipulation.

##  2\. Background

###  2.1. Automatic Differentiation

We are most interested in showing the structure of ad algorithms, so we shall
only give a short intuition for ad. Let $f,g\colon\mathbb{R}\to\mathbb{R}$ be
smooth functions (i.e. infinitely differentiable at all points). The chain
rule states that $\left(f\circ
g\right)^{\prime}(x)=f^{\prime}\left(g(x)\right)\cdot g^{\prime}(x)$. ad
algorithms use this compositional property to incrementally calculate the
derivative of an entire program one basic operation at a time during
evaluation. We refer the reader to the textbook of Griewank and Walther
(Griewank and Walther, 2008) for general knowledge and to Hascoët and Araya-
Polo (Hascoët and Araya-Polo, 2006) for checkpointed reverse mode, our most
interesting example.

###  2.2. Effects and Handlers

Effects and handlers are a structured method of including side-effects into
programs. Algebraic effects were introduced in 2001 by Plotkin and Power
(Plotkin and Power, 2001) handlers for them in 2009 by Plotkin and Pretnar
(Plotkin and Pretnar, 2009). Effects and handlers can be viewed as an
extension of the common feature of catchable exceptions. Catching an exception
terminates the program delimited by the exception handling code, but effect
handlers can resume the handled code and pass a value to it. Effects and
handlers can implement many common side effects such as state, exceptions,
non-determinism, logging, and input-output.

###  2.3. Frank

We will be using the Frank language to implement ad. Frank’s typing and
operational semantics are inspired by call-by-push-value (Levy, 2003), meaning
there is a distinction between values and computations. We note Frank has a
fixed left-to-right evaluation order. Frank combines the concepts of functions
and handlers by unifying them into what Frank refers to as operators, which
act by application. However, we shall usually say handler for operators which
handle effects and functions otherwise. We shall also simplify certain aspects
for ease of exposition, see Convent et al. (Convent et al., 2020) for a
tutorial and details.

Let us consider a simple example of a handler for a program which uses state
of type S.

| state : {S -> <State S>X -> [Console]X}| state _ x = print "end"; x| state s
<get -> k> = print "get"; state s (k s)| state _ <put s -> k> = print "put";
state s (k unit)We first explain the type of state. The handler state takes
two arguments, one of type S and one of type X. In order for state to be used,
the context in which it is called must support the ability [Console] which is
a snoc-list containing exactly one instance Console of the interface Console
(the ability [Console, Console] contains two distinct instances of the same
interface). The ability [Console] means we can use the command print defined
by the interface Console. In the term state s x, the value produced by s can
only be computed using commands from the instances in the ability [Console].
On the other hand, the value produced by x can use commands from [Console,
State S]. The value x has access to State commands because the adjustment
<State S> extends the ambient ability [Console]. We note that the adjustment
<State S> guarantees that state handles all commands of the State interface
(get and set). The full type of state includes braces, showing that state is a
suspended computation. Frank automatically inserts these if they are absent.

We shall briefly explain some aspects of Frank’s operational semantics before
we go into more detail during ad examples. Consider the example top-level use
of state where semicolon is sequencing and postfix ! is nullary function
application.

| 2 + (state 1 (put (_get!_ \+ get!); get!))The ability [Console] is permitted
at the top-level as Frank’s implementation will handle it. As the program
executes, the underlined get is encountered and a continuation of the program
delimited by state is captured, namely the operator {r -> (put (r + get!);
get!)}, and bound to k in the body of the second line of state’s definition.
Once the execution of (put (get! + get!); get!) finishes, the first line of
state’s definition is matched and state exits.

##  3\. Algorithm Implementations

We will cover the implementation of four different handlers in Frank:

evaluate:

: the most basic handler which dispatches to builtin arithmetic operations;

diff:

: an implementation of forward mode ad;

reverse:

: an implementation of reverse mode ad which makes use of the builtin mutable
state interface; and

reversec:

: an implementation of checkpointed reverse mode ad which extends reverse.

Each of the handlers handle the interface Smooth, which conceptually
corresponds to smooth functions on the real numbers. We only include
constants, negation, addition, and multiplication for simplicity, but any
number of other smooth functions could be included. Additionally, Frank
currently does not support floats, so we use integers instead, however with
language support floats could be used.

| data Nullary = constE Int| data Unary = negateE| data Binary = plusE | timesE| | interface Smooth X =| ap0 : Nullary -> X| | ap1 : Unary -> X -> X| | ap2 : Binary -> X -> X -> XThe above definition says the Smooth interface is parameterized by X and has three effectful commands. The command apN is the N-ary application of a smooth function. Note that the nullary functions are constants. For ease of use, we define the following helper functions.

| c : Int -> [Smooth X] X| c i = ap0 (constE i)| | n : X -> [Smooth X] X| n x = ap1 negateE x| | p : X -> X -> [Smooth X] X| p x y = ap2 plusE x y| | t : X -> X -> [Smooth X] X| t x y = ap2 timesE x yThe operational semantics of Frank allows us to treat the above helper functions as if they were commands themselves, which we will do throughout. We will also define helper functions for the dispatching of $n$-ary functions and their derivatives to make the similarity between different ad modes more apparent.

| op0 : Nullary -> [Smooth X] X| op1 : Unary -> X -> [Smooth X] X| op2 : Binary -> X -> X -> [Smooth X] X| op0 (constE i) = c i| op1 negateE x = n x| op2 plusE x y = p x y| op2 timesE x y = t x y| | der1 : Unary -> X -> [Smooth X] X| der2L : Binary -> X -> X -> [Smooth X] X| der2R : Binary -> X -> X -> [Smooth X] X| der1 negateE x = n (c 1) $\nicefrac{{d}}{{dx}}(-x)\ =\ -1$| der2L plusE x y = c 1 $\nicefrac{{d}}{{dx}}(x\ +\ y)\ =\ 1$| der2L timesE x y = y $\nicefrac{{d}}{{dx}}(x\ \cdot\ y)\ =\ y$| der2R plusE x y = c 1 $\nicefrac{{d}}{{dy}}(x\ +\ y)\ =\ 1$| der2R timesE x y = x $\nicefrac{{d}}{{dy}}(x\ \cdot\ y)\ =\ x$

###  3.1. Evaluation

The most basic handler we will consider is the evaluate handler. It only
handles Smooth X where X is instantiated to Int.

| evaluate : <Smooth Int> X -> X| evaluate x = x| evaluate <ap0 (constE i) ->
k> = evaluate (k i)| evaluate <ap1 negateE x -> k> = evaluate (k (-x))|
evaluate <ap2 plusE x y -> k> = evaluate (k (x + y))| evaluate <ap2 timesE x y
-> k> = evaluate (k (x * y))In the case of constE i, its integer parameter i
is returned. Each other case of evaluate takes the integer arguments passed to
the command and performs the corresponding integer operation.

The evaluate handler will always be our top-level handler, and it is the only
way to remove all Smooth interfaces. We shall evaluate an example program
where evaluate is the top-level handler to illustrate how Frank executes. We
will be paying special attention to how delimited continuations are captured.
We will use underlining to show what term is currently at the focus of
evaluation.

Our initial program is below, and represents the term $1+x^{3}+-y^{2}$
evaluated at $x=2$ and $y=4$, which equals $-7$ .

| evaluate (p (c 1) (p (t (t 2 2) 2) (n (t 4 4))))The current focus of
evaluation is the command c 1.

| evaluate (p  _(c 1)_ (p (t (t 2 2) 2) (n (t 4 4))))The argument 1 is in
normal form (fully evaluated). Therefore, we can handle the command c 1. The
handling process begins by capturing the proper delimited continuation by
incrementally freezing the stack of evaluation frames. We represent freezing
by highlighting and boldface.

| evaluate (p  _(c 1)_ (p (t (t 2 2) 2) (n (t 4 4))))

| evaluate (p  _(c 1)_ (p (t (t 2 2) 2) (n (t 4 4))))We have now reached a
handler, evaluate, for the command in focus. The frozen command (highlighted)
is the captured delimited continuation. The ap0 case of evaluate is then
matched to the command c 1, where k is bound to the continuation with c 1
removed and i is bound to 1. The bound variables k and i are then substituted
into the corresponding body of evaluate.

| evaluate  _({x -> (p x (p (t (t 2 2) 2) (n (t 4 4))))} 1)_The next step
applies the continuation to 1.

| evaluate (p 1 (p (t (t 2 2) 2) (n (t 4 4))))The focus of evaluation now
moves to t 2 2, and a new delimited continuation is dynamically captured.

| evaluate (p 1 (p (t  _(t 2 2)_ 2) (n (t 4 4))))

| evaluate (p 1 (p (t  _(t 2 2)_ 2) (n (t 4 4))))

| evaluate (p 1 (p (t  _(t 2 2)_ 2) (n (t 4 4))))

| evaluate (p 1 (p (t  _(t 2 2)_ 2) (n (t 4 4))))

| evaluate (p 1 (p (t  _(t 2 2)_ 2) (n (t 4 4))))We have now again reached the
evaluate handler, and this time match the ap2 case, resulting in the
following.

| evaluate ({x -> (p 1 (p (t x 2) (n (t 4 4))))}  _(2 * 2)_)

| evaluate  _({x -> (p 1 (p (t x 2) (n (t 4 4))))} 4)_

| evaluate (p 1 (p (t 4 2) (n (t 4 4))))Evaluation will continue as such until
the final answer of $-7$ is calculated.

We have now seen how the evaluate handler interprets Smooth commands with the
builtin arithmetic operations. Even though evaluate is simple, it allows us to
write our other handlers in a polymorphic fashion independent of Int.

###  3.2. Forward mode

Our next handler is the diff handler, which implements forward mode ad via a
method known as dual numbers. A dual number is a pair of real numbers where
the second number represents the derivative of the first. The diff handler
handles commands with dual number arguments. The mathematical justification of
ad is not our focus, and thus we shall just focus on the patterns of
computation present without proving their correctness. We define the Dual
datatype and diff below.

| data Dual X = dual X X| | v : Dual X -> X| v (dual x _) = x| | dv : Dual X -> X| dv (dual _ dx) = dx| | diff : <Smooth (Dual X)> Y -> [Smooth X] Y| diff x = x| diff <ap0 n -> k> =| let r = dual (op0 n) (c 0) in| diff (k r)| diff <ap1 u (dual x dx) -> k> =| let r = dual (op1 u x) (t (der1 u x) dx) in| diff (k r)| diff <ap2 b (dual x dx) (dual y dy) -> k> =| let r = dual (op2 b x y) (p (t (der2L b x y) dx)| (t (der2R b x y) dy)) in| diff (k r)Notice the similarities between each of the apN cases. The command being handled by diff is evaluated with opN in the first component of Dual, and a calculation involving derivatives creates the second component.

We will evaluate an example program similar to our previous one. The program
will represent the same mathematical term $1+x^{3}+-y^{2}$ evaluated at $x=2$
and $y=4$, but additionally we shall be calculating the derivative with
respect to $x$ at this point, which is $12$. This is achieved by setting $x$
to dual 2 1 and $y$ to dual 4 0, where $x$ has its second component set to $1$
to treat it as the differentiated variable and $y$ has its second component
set to $0$ to treat it as a constant.

| evaluate (diff (| p (c 1) (p (t (t (dual 2 1) (dual 2 1)) (dual 2 1))| (n (t
(dual 4 0) (dual 4 0))))| ))

Evaluation begins as before, with the c 1 command being in focus and a
delimited continuation being captured.

| evaluate (diff (| p  _(c 1)_ (p (t (t (dual 2 1) (dual 2 1)) (dual 2 1))| (n
(t (dual 4 0) (dual 4 0))))| ))Note how the continuation captured is delimited
by diff and not evaluate. This behavior is due to the effect typing system of
Frank. There are two different instances of the Smooth interface available to
the portion of the program being handled. By default, the innermost handler
provides the instance being used by extending the ambient ability with an
adaptor. As we shall see later, Frank provides constructs allowing us to
select handlers other than the innermost. The top case of diff is matched by c
1 with the following result.

| evaluate (| let r = dual  _(op0 (constE 1))_ (c 0) in| diff (| {x -> (p x (p
(t (t (dual 2 1) (dual 2 1)) (dual 2 1))| (n (t (dual 4 0) (dual 4 0)))))} r)|
)

| evaluate (| let r = dual (c 1) (c 0) in| diff (| {x -> (p x (p (t (t (dual 2
1) (dual 2 1)) (dual 2 1))| (n (t (dual 4 0) (dual 4 0)))))} r)| )We now have
two c commands which will be be handled by evaluate, producing dual 1 0 for
r’s value. After handling, r will be be substituted and the continuation
applied.

| evaluate (diff (| p (dual 1 0) (p (t  _(t (dual 2 1) (dual 2 1))_ (dual 2
1))| (n (t (dual 4 0) (dual 4 0))))| ))Evaluation will then continue in a
similar manner for all remaining commands. Each command will first be handled
by diff, and the commands in the body of each diff case handled by evaluate,
eventually producing dual -7 12.

We will now focus on Frank’s ability to dynamically determine which handler
handles a command. First, we define two auxiliary functions.

| lift : X -> [Smooth X, Smooth (Dual X)] (Dual X)| lift x = dual x (<Smooth> (c 0))| | d : {(Dual X) -> [Smooth X, Smooth (Dual X)] (Dual X)}| -> X -> [Smooth X] X| d f x = dv (diff (f (dual x (<Smooth> (c 1)))))The adaptor <Smooth> in lift causes the command c 0 to be associated with Smooth X and not the rightmost instance Smooth (Dual X). The d function returns the derivative of a unary function and lift will enable us to nest d. Note that as in lift, <Smooth> in d causes the command c 1 to be associated with Smooth X. Consider the expression $\nicefrac{{d}}{{dx}}(x\cdot\nicefrac{{d}}{{dy}}(x+y)|_{y=1})|_{x=1}$ (which equals $1$). The corresponding program requires lift.

| evaluate (d {x -> t x (d {y -> p (lift x) y} (c 1))}  _(c 1)_)We evaluate
until the delimited continuation is captured.

| evaluate  _(d{x -> t x (d {y -> p (lift x) y} (c 1))} 1)_

| evaluate (dv (diff (| {x -> t x (d {y -> p (lift x) y} (c 1))}| (dual 1
(<Smooth>  _(c 1)_))| )))

| evaluate (dv (diff (| {x -> t x (d {y -> p (lift x) y} (c 1))}| (dual 1
(<Smooth>  _(c 1)_))| )))The continuation for c 1 is delimited by evaluate due
to <Smooth>. We conclude by noting that Frank will reject the nested program
if lift is not present.

###  3.3. Reverse mode

The evaluate and diff handlers manipulate programs by capturing delimited
continuations, but only in quite simple ways. They each eventually compute a
value based on the command being handled and then continue with the original
program with the computed value substituted in. The reverse handler will be
different, and will build up a secondary program during the evaluation of the
initial program.

Reverse mode ad works by creating a mutable cell for each value which
accumulates contributions to its derivative. The method of accumulation is a
generalized version of the backpropagation algorithm made prominent by machine
learning. We define the datatype Prop for backpropagation where Ref X is a
reference to a mutable cell containing a value of type X. The reverse handler
handles commands containing Prop’s.

| data Prop X = prop X (Ref X)| | fwd : Prop X -> X| fwd (prop x _) = x| | deriv : Prop X -> Ref X| deriv (prop _ r) = r| | reverse : <Smooth (Prop X)> Unit -> [RefState, Smooth X] Unit| reverse x = x| reverse <ap0 n -> k> =| let r = prop (op0 n) (new (c 0)) in| reverse (k r)| reverse <ap1 u (prop x dx) -> k> =| let r = prop (op1 u x) (new (c 0)) in| reverse (k r);| write dx (p (read dx) (t (der1 u x) (read (deriv r))))| reverse <ap2 b (prop x dx) (prop y dy) -> k> =| let r = prop (op2 b x y) (new (c 0)) in| reverse (k r);| write dx (p (read dx) (t (der2L b x y) (read (deriv r))));| write dy (p (read dy) (t (der2R b x y) (read (deriv r))))The reverse handler makes use of the same op and der functions as diff, but is different from evaluate and diff in two important ways. Firstly, the type of reverse shows that it requires access to the RefState interface of mutable state (a builtin effect of Frank that can be handled by the language implementation). Secondly, the body of the ap1 and ap2 cases contains code after the use of the captured delimited continuation k. We shall see these writes to memory will form the secondary program which actually accumulates derivatives.

To properly calculate derivatives with reverse, we require a small helper
function which starts the process of backpropagation, which we call grad for
gradient.

| grad : {(Prop X)| -> [RefState, Smooth X, Smooth (Prop X)] (Prop X)}| -> X
-> [RefState, Smooth X] X| grad f x =| let z = prop x (new (c 0)) in| reverse
(write (deriv (f z)) (<Smooth> (c 1)));| read (deriv z)We evaluate the same
term as before.

| evaluate (grad ({x ->| let y = c 4 in p (c 1) (p (t (t x x) x) (n (t y y)))|
} 2))

| evaluate (| let z = prop 2 (new (c 0)) in| reverse (write (deriv ({x ->| let
y = c 4 in p (c 1) (p (t (t x x) x) (n (t y y)))| } z)) (<Smooth> (c 1)));|
read (deriv z))The term new (c 0) is handled first by evaluate for c 0
(returning 0), and the command new 0 is handled by the Frank implementation
and returns a new reference <z> whose cell contains 0. The result is then
substituted for z.

| evaluate (| reverse (write (deriv  _({x ->_|  _let y = c 4 in p (c 1) (p (t (t x x) x) (n (t y y)))_ |  _} (prop 2 <z>))_) (<Smooth> (c 1)));| read (deriv (prop 2 <z>)))Next, the anonymous function is applied to prop 2 <z>.

| evaluate (| reverse (write (deriv (| let y =  _c 4_ in| p (c 1) (p (t (t
(prop 2 <z>) (prop 2 <z>)) (prop 2 <z>))| (n (t y y)))| )) (<Smooth> (c 1)));|
read (deriv (prop 2 <z>)))The command c 4 is handled by the ap0 case of
reverse, which as before creates a new reference <r1>, and thus y is
substituted by prop 4 <r1>. The command c 1 will create <r2>.

| evaluate (| reverse (write (deriv (| p (prop 1 <r2>)| (p (t  _(t (prop 2
<z>) (prop 2 <z>))_ (prop 2 <z>))| (n (t (prop 4 <r1>) (prop 4 <r1>))))| ))
(<Smooth> (c 1)));| read (deriv (prop 2 <z>)))We have now reached the first
interesting command, which matches the ap2 case of reverse. The captured
delimited continuation is now explicitly highlighted.

| evaluate (| reverse (write (deriv (| p (prop 1 <r2>) | (p (t  _(t (prop 2 <z>) (prop 2 <z>))_ (prop 2 <z>))| (n (t (prop 4 <r1>) (prop 4 <r1>)))) | )) (<Smooth> (c 1)));| read (deriv (prop 2 <z>)))The result of reverse handling the command produces a new reference <r3>.

| evaluate (| reverse (write (deriv (| p (prop 1 <r2>)| (p (t (prop 4 <r3>)
(prop 2 <z>))| (n (t (prop 4 <r1>) (prop 4 <r1>))))| )) (<Smooth> (c 1)));|
write <z> (p (read <z>)| (t (der2L timesE 2 2) (read (deriv (prop 4
<r3>)))));| write <z> (p (read <z>)| (t (der2R timesE 2 2) (read (deriv (prop
4 <r3>)))));| read (deriv (prop 2 <z>)))We see that the evaluation of the
initial program has produced new expressions to be evaluated after the initial
program finishes. The handling by reverse will eventually handle all commands
meant for it, producing the following.

| evaluate (| reverse (write <r8> (<Smooth> (c 1)));| write <r2> (p (read
<r2>)| (t (der2L plusE 1 -8) (read (deriv (prop -7 <r8>)))));| write <r7> (p
(read <r7>)| (t (der2R plusE 1 -8) (read (deriv (prop -7 <r8>)))));| write
<r4> (p (read <r4>)| (t (der2L plusE 8 -16) (read (deriv (prop -8 <r7>)))));|
write <r6> (p (read <r6>)| (t (der2R plusE 8 -16) (read (deriv (prop -8
<r7>)))));| write <r5> (p (read <r5>)| (t (der1 negateE 16) (read (deriv (prop
-16 <r6>)))));| write <r1> (p (read <r1>)| (t (der2L timesE 4 4) (read (deriv
(prop 16 <r5>)))));| write <r1> (p (read <r1>)| (t (der2R timesE 4 4) (read
(deriv (prop 16 <r5>)))));| write <r3> (p (read <r3>)| (t (der2L timesE 4 2)
(read (deriv (prop 8 <r4>)))));| write <z> (p (read <z>)| (t (der2R timesE 4
2) (read (deriv (prop 8 <r4>)))));| write <z> (p (read <z>)| (t (der2L timesE
2 2) (read (deriv (prop 4 <r3>)))));| write <z> (p (read <z>)| (t (der2R
timesE 2 2) (read (deriv (prop 4 <r3>)))));| read (deriv (prop 2 <z>)))The
above code is the secondary program created by reverse, which performs
backpropagation. Furthermore, if a user wished to capture this secondary
program, the definition of reverse could be changed to return a suspended
computation. Thus, we could also partially evaluate the whole program (initial
and backpropagation) by running only the initial program and capturing the
backpropagation computation.

It could also be possible to use multi-stage programming by reifying the
initial and secondary programs as a computation graph in the style of Wang et
al. (Wang et al., 2019). Their approach uses delimited continuations and
combines normal execution with building an intermediate representation. As
effects and handlers are essentially a structured use of delimited
continuations, a similar story for Frank may be possible.

###  3.4. Checkpointed reverse mode

The final algorithm we shall cover is checkpointed reverse mode. Reverse mode
has maximum memory residency proportional to the number of operations (as seen
in the definition of reverse). Checkpointed reverse mode allows a trade-off
between space and time by recomputing checkpointed subprograms, once without
allocating memory and an additional time with memory. However, any memory
allocated in between these two runs can be safely deallocated, as it
corresponds to code after the checkpointed subprogram in the original program,
thus reducing maximum memory residency.

To define our new handler, we introduce a Checkpoint effect which takes a
suspended computation that will be run multiple times. We also define a simple
evaluate like handler, evaluatet (see appendix for definition).

| interface Checkpoint X =| checkpoint :| {[Checkpoint X , Smooth (Prop X)]
Prop X} -> Prop XFrank also contains a catch-all pattern match <m> which
matches values and commands not handled above it. We use this feature to
extend reverse by delegating any Smooth commands received to reverse and only
adding a case for checkpoint.

| reversec : <Checkpoint X, Smooth (Prop X)> Unit| -> [RefState, Smooth X]
Unit| reversec x = x| reversec <checkpoint p -> k> =| let s = new (c 0) in|
let res = <RefState> (evaluatet s (| <Smooth(s a b -> s b)> p!| )) in| let r =
prop (fwd res) (new (c 0)) in| reversec (k r);| reversec (write| (deriv
(<Smooth(s a b -> s b), RefState> p!))| (read (deriv r)))| reversec <m> =
reversec (<Smooth(s a -> s)> (reverse m!))Note how the checkpointed subprogram
(the suspended computation p which is the argument of checkpoint) is called
twice, once with evaluatet as the handler and once with reversec as the
handler. Additionally, the last case will match every Smooth command, and then
reinvoke the captured computation with a new reverse handler to handle the
command.

Consider the following program where gradc is grad with reversec in the place
of reverse.

| evaluate (gradc ({x ->| let y = c 2 in| let z =  _checkpoint{p x y}_ in| let
a = checkpoint {let w = checkpoint {t x z} in p w y} in| p a x| } (c 2)))The
first interesting evaluation step is after the underlined checkpoint has been
handled.

| evaluate (| reversec (<Smooth(s a -> s)> (reverse (write (deriv (| let z =
prop 4 <r2> in| let a = checkpoint {| let w = checkpoint t (prop 2 <z>) z in|
p w (prop 2 <r1>)} in| p a (prop 2 <z>)| )) (<Smooth> (c 1)))));| reversec
(write (deriv (<Smooth(s a b -> s b), RefState>|  _{ p (prop 2 <z>) (prop 2
<r1>)}_!))| (read (deriv (prop 4 <r2>))));| read (deriv (prop 2 <z>)))Note how
on the second line the reverse handler has been made the innermost delimiter
of the remainder of the initial program, via the catch-all case of reversec.
Additionally, note how the checkpointed code (underlined) is stored as a thunk
to be run after the initial program in the second use of reversec. After the
initial program has been evaluated away, we obtain the following.

| evaluate (| reversec (<Smooth(s a -> s)> (| reverse (write <r4> 1);| write
<r3> (p (read <r3>)| (t (der2L plusE 10 2) (read (deriv (prop 12 <r4>)))));|
write <z> (p (read <z>)| (t (der2R plusE 10 2) (read (deriv (prop 12
<r4>))))));| reversec (write (deriv (<Smooth(s a b -> s b), RefState>| {let w
=  _checkpoint t (prop 2 <z>) (prop 4 <r2>)_ in| p w (prop 2 <r1>)}!))| (read
(deriv (prop 10 <r3>))));| reversec (write (deriv (<Smooth(s a b -> s b),
RefState>| {p (prop 2 <z>) (prop 2 <r1>)}!))| (read (deriv (prop 4 <r2>))));|
read (deriv (prop 2 <z>)))The remaining checkpoint command illustrates the
recursive nature of reversec. It shows how even nested checkpointing in
checkpointed code can be properly evaluated by delaying the program
transformation happening via evaluation.

##  4\. Conclusion

We have seen the implementation and evaluation of ad in Frank via Frank’s
operation semantics and four handlers: evaluate, diff, reverse, and reversec.
While evaluate and diff do effectively no program transformations, reverse and
reversec build up ancillary programs via delimited continuations. The effects
and handler style of Frank allowed us to compose and nest our defined
handlers, which is especially apparent in the modular definition of reversec
which delegates all Smooth commands to reverse. It may also be possible to
integrate multi-stage programming by using the system of Wang et al.. In
conclusion, we have illustrated in Frank that effects and handlers are a good
match for ad, and that effects and handlers can be seen as a form of program
manipulation.

###### Acknowledgements.

I would like to thank Sam Lindley for answering my many questions about Frank,
my supervisor Chris Heunen for his support, and Ohad Kammar for conversations
about this work and encouragement to improve it. I would also like to thank
the reviewers for their valuable feedback.

## References

  * (1)
  * Bischof et al. (1996) Christian Bischof, Peyvand Khademi, Andrew Mauer, and Alan Carle. 1996.  Adifor 2.0: Automatic Differentiation of Fortran 77 Programs.  _IEEE Comput. Sci. Eng._ 3, 3 (Sept. 1996), 18–32.  https://doi.org/10.1109/99.537089
  * Bischof et al. (1997) C. H. Bischof, L. Roh, and A. J. Mauer-Oats. 1997.  ADIC: an extensible automatic differentiation tool for ANSI-C.  _Software: Practice and Experience_ 27, 12 (1997), 1427–1456.  https://doi.org/10.1002/(SICI)1097-024X(199712)27:12<1427::AID-SPE138>3.0.CO;2-Q
  * Convent et al. (2020) Lukas Convent, Sam Lindley, Conor Mcbride, and Craig Mclaughlin. 2020.  Doo bee doo bee doo.  _Journal of Functional Programming_ 30 (2020).  https://doi.org/10.1017/S0956796820000039 Publisher: Cambridge University Press.
  * Griewank and Walther (2008) A. Griewank and A. Walther. 2008.  _Evaluating Derivatives_.  Society for Industrial and Applied Mathematics.  https://doi.org/10.1137/1.9780898717761
  * Hascoët and Araya-Polo (2006) Laurent Hascoët and Mauricio Araya-Polo. 2006.  Enabling user-driven Checkpointing strategies in Reverse-mode Automatic Differentiation.  _arXiv:cs/0606042_ (June 2006).  http://arxiv.org/abs/cs/0606042 arXiv: cs/0606042.
  * Hascoët and Pascual (2013) Laurent Hascoët and Valérie Pascual. 2013.  The Tapenade automatic differentiation tool: Principles, model, and specification.  _ACM Trans. Math. Softw._ 39, 3 (May 2013), 20:1–20:43.  https://doi.org/10.1145/2450153.2450158
  * Levy (2003) P. B. Levy. 2003\.  _Call-By-Push-Value: A Functional/Imperative Synthesis_.  Springer Netherlands.  https://doi.org/10.1007/978-94-007-0954-6
  * Lindley et al. (2017) Sam Lindley, Conor McBride, and Craig McLaughlin. 2017\.  Do be do be do. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ _(POPL 2017)_. Association for Computing Machinery, Paris, France, 500–514.  https://doi.org/10.1145/3009837.3009897
  * Pascual and Hascoët (2008) Valérie Pascual and Laurent Hascoët. 2008.  TAPENADE for C. In _Advances in Automatic Differentiation_ _(Lecture Notes in Computational Science and Engineering)_ , Christian H. Bischof, H. Martin Bücker, Paul Hovland, Uwe Naumann, and Jean Utke (Eds.). Springer, Berlin, Heidelberg, 199–209.  https://doi.org/10.1007/978-3-540-68942-3_18
  * Plotkin and Power (2001) Gordon Plotkin and John Power. 2001.  Adequacy for Algebraic Effects.  In _Foundations of Software Science and Computation Structures_ , Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Furio Honsell, and Marino Miculan (Eds.). Vol. 2030. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–24.  https://doi.org/10.1007/3-540-45315-6_1 Series Title: Lecture Notes in Computer Science.
  * Plotkin and Pretnar (2009) Gordon Plotkin and Matija Pretnar. 2009.  Handlers of Algebraic Effects.  In _Programming Languages and Systems_ , Giuseppe Castagna (Ed.). Vol. 5502. Springer Berlin Heidelberg, Berlin, Heidelberg, 80–94.  https://doi.org/10.1007/978-3-642-00590-9_7 Series Title: Lecture Notes in Computer Science.
  * Speelpenning (1980) Bert Speelpenning. 1980\.  _Compiling fast partial derivatives of functions given by algorithms_.  Ph.D. University of Illinois at Urbana-Champaign, USA.  AAI8017989.
  * Wang et al. (2019) Fei Wang, Daniel Zheng, James Decker, Xilun Wu, Grégory M. Essertel, and Tiark Rompf. 2019.  Demystifying differentiable programming: shift/reset the penultimate backpropagator.  _Proc. ACM Program. Lang._ 3, ICFP (July 2019), 96:1–96:31.  https://doi.org/10.1145/3341700
  * Wengert (1964) R. E. Wengert. 1964\.  A simple automatic derivative evaluation program.  _Commun. ACM_ 7, 8 (Aug. 1964), 463–464.  https://doi.org/10.1145/355586.364791

## Appendix

The following is the definition of evaluatet use in reversec. Note the
similarities with evaluate.

| evaluatet : Ref X| -> <Checkpoint X, Smooth (Prop X)> Y| -> [Smooth X] Y|
evaluatet _ x = x| evaluatet s <checkpoint p -> k> =| let res = evaluatet s
(<Smooth(s a b -> s b)> p!) in| evaluatet s (k (prop (fwd res) s))| evaluatet
s <ap0 n -> k> =| evaluatet s (k (prop (<Smooth> (op0 n)) s))| evaluatet s
<ap1 u (prop x dx) -> k> =| evaluatet s (k (prop (<Smooth> (op1 u x)) s))|
evaluatet s <ap2 b (prop x dx) (prop y dy) -> k> =| evaluatet s (k (prop
(<Smooth> (op2 b x y)) s))