# Mechanized Relational Verification of Concurrent Programs with Continuations - Iris Project

←

**Page content transcription**

If your browser does not render page correctly, please read the page content below

105 Mechanized Relational Verification of Concurrent Programs with Continuations AMIN TIMANY, imec-Distrinet, KU Leuven, Belgium LARS BIRKEDAL, Aarhus University, Denmark Concurrent higher-order imperative programming languages with continuations are very flexible and allow for the implementation of sophisticated programming patterns. For instance, it is well known that continuations can be used to implement cooperative concurrency. Continuations can also simplify web server implementa- tions. This, in particular, helps simplify keeping track of the state of server’s clients. However, such advanced programming languages are very challenging to reason about. One of the main challenges in reasoning about programs in the presence of continuations is due to the fact that the non-local flow of control breaks the bind rule, one of the important modular reasoning principles of Hoare logic. In this paper we present the first completely formalized tool for interactive mechanized relational verification of programs written in a concurrent higher-order imperative programming language with continuations (call/cc and throw). We develop novel logical relations which can be used to give mechanized proofs of relational properties. In particular, we prove correctness of an implementation of cooperative concurrency with continuations. In addition, we show that that a rudimentary web server implemented using the continuation- based pattern is contextually equivalent to one implemented without the continuation-based pattern. We introduce context-local reasoning principles for our calculus which allows us to regain modular reasoning principles for the fragment of the language without non-local control flow. These novel reasoning principles can be used in tandem with our (non-context-local) Hoare logic for reasoning about programs that do feature non-local control flow. Indeed, we use the combination of context-local and non-context-local reasoning to simplify reasoning about the examples. CCS Concepts: • Theory of computation → Logic and verification; Hoare logic; Separation logic; Program specifications; Program verification; Invariants; Pre- and post-conditions; • Software and its engineering → Formal software verification; Semantics. Additional Key Words and Phrases: Logical relations, Continuations, Concurrency ACM Reference Format: Amin Timany and Lars Birkedal. 2019. Mechanized Relational Verification of Concurrent Programs with Continuations. Proc. ACM Program. Lang. 3, ICFP, Article 105 (August 2019), 28 pages. https://doi.org/10.1145/ 3341709 1 INTRODUCTION In a programming language with continuations, a computation can be suspended into a continuation object which can be resumed later. Continuations enable interesting programming patterns. For instance, it is well-known that they can be used to implement cooperative concurrency [Haynes et al. 1984]: switching between threads can be implemented by suspending the running thread, storing the suspension and running another thread. Another notable application of continuations Authors’ addresses: Amin Timany, Department of Computer Science, imec-Distrinet, KU Leuven, Leuven, Belgium, amin. timany@cs.kuleuven.be; Lars Birkedal, Department of Computer Science, Aarhus University, Aarhus, Denmark, birkedal@ cs.au.dk. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). © 2019 Copyright held by the owner/author(s). 2475-1421/2019/8-ART105 https://doi.org/10.1145/3341709 Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:2 Amin Timany and Lars Birkedal is the implementation of continuation-based web servers [Flatt 2017; Krishnamurthi et al. 2007; Queinnec 2004]. Web servers store the state of their communication with each client in order to provide a coherent experience for returning clients. For this purpose continuation-based web servers store the continuation of the server-side program. This helps simplify the web server program because the only thing that the server needs to do in order to serve a returning client appropriately is to resume the continuation corresponding to the last communication with the client. Both of the aforementioned programming patters involve concurrency, higher-order and impera- tive aspects of the programming language in combination with continuations in sophisticated and interesting ways. Such expressive and advanced programming languages and programs written in them are known to be challenging to model and reason about. In this paper we present novel techniques for relational reasoning about such programming languages and programs written in them. Specifically, we develop a new logical relations model for proving contextual refinement of µ,ref programs written in Fconc,cc , a call-by-value programming language featuring concurrency (conc), impredicative polymorphism (F), recursive types (µ), dynamically allocated higher-order store (ref ) and first-class continuations (cc) with call/cc and throw primitives. We employ this logical relations model to prove (1) contextual equivalence of two simple web server implementations: a continuation-based one and a state-storing one; and (2) that one-shot continuations (continuations that can only be used once) can be used to simulate ordinary continuations [Friedman and Haynes 1985]. The latter is a well-known result for sequential programs, see, e.g., Dreyer et al. [2012]. Here µ,ref we show that it also holds in Fconc,cc , that is, in the presence of concurrency. In addition, we develop a relational model for showing the correctness of a continuation-based implementation of cooperative concurrency. We consider two programming languages: a language, µ,ref µ,ref Fcc,coop , with built-in cooperative concurrency (coop) and a sequential language, Fcc , featuring µ,ref µ,ref continuations. We develop a cross-language logical relation between Fcc and Fcc,coop and use it to show correctness of a translation of cooperative concurrency into one based on continuations. We define our logical relations models in a variant of the Iris program logic framework [Jung et al. 2016; JUNG et al. 2018; Jung et al. 2015; Krebbers et al. 2017a]. Iris is a framework for state-of- the-art higher-order concurrent separation logics. We use Iris because (1) it allows us to define our logical relations and reason about them at a higher level of abstraction compared to an explicit model construction; (2) we side-step the well-known type-world-circularity problems [Ahmed 2004; Ahmed et al. 2002; Birkedal et al. 2011] involved in defining logical relations for programming languages with higher-order store (since that is already “taken care of” by the model of Iris); and (3) we can leverage the Coq implementation of the Iris base logic [Krebbers et al. 2017a] and the Iris Proof Mode [Krebbers et al. 2017b] when mechanizing our development in Coq. Indeed, accompanying this paper is a tool for mechanized relational verification of concurrent programs with continuations. The mechanization has been done in Coq and all the results in the paper have been formally verified. Context-local reasoning principles Some of the most important features of concurrent separation logics for modular/local reasoning about concurrent imperative programs, e.g. da Rocha Pinto et al. [2014]; Dinsdale-Young et al. [2013, 2010]; Jung et al. [2016, 2015]; Krebbers et al. [2017a,b]; Ley-Wild and Nanevski [2013]; Nanevski et al. [2014]; O’Hearn [2007]; Sergey et al. [2015]; Svendsen and Birkedal [2014]; Turon et al. [2013a] are thread-local reasoning and context-local reasoning. Thread-local reasoning means that we can reason about each thread in isolation: when we reason about a particular thread, we need not Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:3 explicitly consider interactions from other concurrently executing threads. Similarly, context-local means that when we reason about a particular expression, we need not consider under which evaluation context it is being evaluated. The latter is sometimes codified by the soundness of a proof rule such as the following: Hoare-Bind (inadmissible in presence of continuations) {P } e { Ψ } ∀w. { Ψ(w)} K[w] {Φ } {P } K[e] {Φ } The Hoare-triple {P } e { Ψ } intuitively means that, given precondition P, expression e is safe and, whenever it reduces to a value v, we are guaranteed that Ψ(v) holds. Intuitively, the above rule expresses that to prove a Hoare triple for an expression e in an evaluation context K, it suffices to prove a property for e in isolation from K, and then show that the desired postcondition Φ can be obtained when substituting a value w satisfying the postcondition Ψ for e into the evaluation context. In a programming language with non-local control operators, e.g. call/cc and throw, the context under which a program is being evaluated is of utmost importance, and thus the above proof rule is not sound in general for languages with non-local control operators. In spite of this, we ought be able to reason about those parts of the program that do not feature any non-local control flow operators in a context-local way. We explain this via an example which we use to demonstrate how non-local control flow operators can break context-local reasoning. We then discuss how our context-local program logic allows us to regain context-local reasoning in a sound way, and, how we can employ our context-local program logic to derive a context-local specification for the this example. To illustrate how non-local control flow operators can break context-local reasoning, consider the following program: CallIncr ≜ λ f . let x = ref(0) in let д = f () in x ← ! x + 2; д (); ! x µ,ref (In Section 2 we present the syntax and semantics of Fconc,cc formally; here we simply explain informally what is intended by our ML-like syntax above.) The program CallIncr takes a function f as argument, allocates a local reference with value 0, calls f , and binds its result (again a function) to д. It then increments the internal reference and subsequently calls д before returning the value stored in the internal reference. Intuitively, in a programming language without non-local control flow this program should always return 2 (if it terminates, of course). Hence, using the bind rule we would be able to derive the following (incorrect) specification for CallIncr: {true} h () {x . {true} x () {y. y = ()} } implies {true} CallIncr h {x . x = 2} (CallIncr-incorrect-spec) This specification says that, if h is a function that upon call returns a function x for which we know the Hoare-triple {true} x () {y. y = ()} holds, then CallIncr applied to h should return 2. This specification CallIncr-incorrect-spec does not hold though. For a concrete counter-example, let h to be h = λ_. call/cc (x . λ_. throw (λ. ()) to x) This function, when called, captures the current continuation x and then returns a function that returns to the point x, this time, with the result (λ. ()), a function that simply returns the unit value (). Hence, when CallIncr is called with h, the internal reference of CallIncr wil be incremented twice, and thus return value be 4 and not 2. Notice that for h above we can prove the spec {true} h () {x . {true} x () {y. y = ()} } since this spec considers h in isolation, i.e., the captured continuation will be the empty continuation. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:4 Amin Timany and Lars Birkedal Hence, as expected, the program CallIncr only behaves context-locally if the argument it is applied to does. This is indeed reflected in the context-local specification of CallIncr expressed in terms of context-local Hoare triples (Specification CallIncr-context-local-spec below). We introduce context-local Hoare triples in Section 4. A context-local Hoare triple {P }cl e {x . Q } not only implies safety of e (as ordinary Hoare triples do), but also implies that e behaves context-locally. Hence, they can be used to reason about programs context-locally, and thus the bind rule holds for them. In particular, we can prove the following context-local specification for the program CallIncr above: {true}cl h () {x . {true}cl x () {y. y = ()} } implies {true}cl CallIncr h {x . x = 2} (CallIncr-context-local-spec) This specification captures exactly the intuitive idea explained above: if we know that h, and the function it returns, behave context-locally, then so does CallIncr h. Since context-local Hoare-triples cannot be used to reason about all programs, particularly about non-trivial uses of call/cc and throw, we have to express our logical relations model using ordinary (non-context-local) Hoare-triples, following ideas from earlier work [Krebbers et al. 2017b; Turon et al. 2013a]. In Section 4, we discuss how ordinary (non-context-local) Hoare-triples interact with their context-local counter parts. Using a combination of non-context-local and context-local triples, we can simplify reasoning about contextual equivalence of concurrent programs with continuations using our logical relations model. We achieve this by reasoning about parts of programs that do not use non-local control operators using context-local Hoare-triples. Contributions. In this paper, we make the following contributions: • We present a program logic (weakest preconditions and Hoare-triples) for reasoning about µ,ref programs written in Fconc,cc , a programming language with impredicative polymorphism, recursive types, higher-order functions, higher-order store, concurrency and first-class con- tinuations. • We present context-local weakest-preconditions and Hoare-triples which simplify reasoning about programs without non-local control flow. µ,ref • We present a novel logical relations model for Fconc,cc . • We use our logical relations model and context-local reasoning to prove equivalence of two simple web server implementations: a continuation-based one and a state-storing one. • We further use our logical relations model to prove correctness of Friedman and Haynes [1985] encoding of continuations by means of one-shot continuations in a concurrent programming language. µ,ref µ,ref • We develop a cross-language logical relations model between Fcc and Fcc,coop for proving program refinement. • We use our cross-language logical relations model to prove correctness of a continuation- based implementation of cooperative concurrency. • We have developed a fully formalized tool for mechanized interactive relational verification of concurrent programs with continuations. Our tool is developed on top of Iris, a state-of- the-art program logic framework, and we have used it to mechanize all of our contributions in the Coq proof assistant. µ,ref 2 THE LANGUAGE: Fconc,cc µ,ref The language that we consider in this paper, Fconc,cc , is a typed lambda calculus with a standard call- by-value small-step operational semantics. It features impredicative polymorphism (F), recursive types (µ), higher-order mutable references (ref ), fine-grained concurrency (conc) and first-class Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:5 µ,ref continuations (cc). The types of Fconc,cc are as follows: τ ::= α | 1 | B | N | τ → τ | ∀α . τ | µα . τ | τ × τ | τ + τ | ref(τ ) | cont(τ ) Here α ranges over type variables. The types 1, B and N are the unit type, the type of Boolean values and the type of natural numbers respectively. The type ref(τ ) is the type of references with contents of type τ and cont(τ ) is the type of continuations that can be resumed by throwing them a value of type τ . The symbols ×, +, µ, ∀ and → are the usual product, sum, recursive type, polymorphic type and function type formers, respectively. The syntax for expressions and values is: e ::= x | () | true | false | n | e ⊚ e | rec f(x) = e | e e | Λ e | e _ | fold e | unfold e | (e, e) | πi e | inji e | match e with inji x ⇒ ei end | ℓ | ref(e) | ! e | e ← e | cas(e, e, e) | fork {e} | cont(K) | call/cc (x . e) | throw e to e v ::= () | true | false | n | rec f(x) = e | Λ e | fold v | (v, v) | inji v | ℓ | cont(K) We write n for natural numbers and the symbol ⊚ stands for binary operations on natural numbers (both basic arithmetic operations and basic comparison operations). We consider both recursive functions rec f(x) = e and polymorphic type abstractions Λ e to be values. We write e _ for type level application (e is a polymorphic expression). We use fold and unfold to fold and unfold elements of recursive types. Memory locations ℓ are values of reference types. The expression ! e reads the memory location e evaluates to, and e ← e ′ is an assignment of the value computed by e ′ to the memory location computed by e. The expression fork {e} is for forking off a new thread to compute e and we write cas(e, e ′, e ′′) for the compare-and-set operation. A continuation, cont(K), is essentially a suspended evaluation context (see the operational semantics below). µ,ref Evaluation contexts of Fconc,cc are as follows: K ::= [ ] | K ⊚ e | v ⊚ K | K e | v K | K _ | fold K | unfold K | if K then e else e | (K, e) | (v, K) | πi K | inji K | match K with inji x ⇒ ei end | ref(K) | ! K | K ← e | v ← K | cas(K, e, e) | cas(v, K, e) | cas(v, v, K) | throw K to e | throw v to K The evaluation context [ ] is the empty evaluation context. 2.1 Typing An excerpt of the typing rules is depicted in Figure 1. The context Ξ = α 1, . . . , α n is a list of distinct type variables and the context Γ = x 1 : τ1, . . . x n : τn assigns types to program variables. 2.2 Operational semantics µ,ref We define the call-by-value small-step operational semantics of Fconc,cc in two stages. We first define a head-step relation →K . Here, K is the context under which the head step is being performed. Based on this, we define the operational semantics of programs by what we call the thread-pool step relation →. A thread pool reduces by making a head reduction step in one of the threads, by forking off a new thread, or by resuming a captured continuation in one of the threads. These rules are depicted in Figure 2. In this figure, σ is the physical state of the program, i.e., the program heap, which is a finite partial map from memory locations to values. An excerpt of the head-step relation is given in Figure 3. Notice that the head-step for call/cc captures the continuation that is the index of the head-step relation. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:6 Amin Timany and Lars Birkedal Ξ| Γ ⊢e :τ T-Var T-TLam x :τ ∈ Γ T-Unit T-Nat Ξ, α | Γ ⊢ e : τ Ξ| Γ ⊢x :τ Ξ | Γ ⊢ () : 1 Ξ| Γ ⊢n:N Ξ | Γ ⊢ Λ e : ∀α . τ T-Rec T-App T-TApp Ξ | Γ, x : τ , f : τ → τ ′ ⊢ e : τ ′ Ξ | Γ ⊢ e : τ → τ′ Ξ | Γ ⊢ e′ : τ Ξ | Γ ⊢ e : ∀α . τ Ξ | Γ ⊢ | rec f(x) = e : τ → τ ′ Ξ| Γ ⊢ee :τ ′ ′ Ξ | Γ ⊢ e _ : τ [τ ′/α] T-Fold T-UnFold T-Ref Ξ | Γ ⊢ e : τ [µα . τ /α] Ξ | Γ ⊢ e : µα . τ Ξ| Γ ⊢e :τ Ξ | Γ ⊢ fold e : µα . τ Ξ | Γ ⊢ unfold e : τ [µα . τ /α] Ξ | Γ ⊢ ref(e) : ref(τ ) T-DeRef T-Fork T-Assign Ξ | Γ ⊢ e : ref(τ ) Ξ| Γ ⊢e :τ Ξ | Γ ⊢ e : ref(τ ) Ξ | Γ ⊢ e′ : τ Ξ | Γ ⊢ !e : τ Ξ | Γ ⊢ fork {e} : 1 Ξ | Γ ⊢ e ← e′ : 1 T-CAS T-Call/cc Ξ | Γ ⊢ e 1 : ref(τ ) Ξ | Γ ⊢ e2 : τ Ξ | Γ ⊢ e3 : τ Ξ | Γ, x : cont(τ ) ⊢ e : τ Ξ | Γ ⊢ cas(e 1, e 2, e 3 ) : B Ξ | Γ ⊢ call/cc (x . e) : τ T-Throw Ξ| Γ ⊢e :τ Ξ | Γ ⊢ e ′ : cont(τ ) Ξ | Γ ⊢ throw e to e ′ : τ ′ Fig. 1. An excerpt of the typing rules (® e ′; σ ′) e ; σ ) → (® (e, σ ) →K (e ′, σ ′) e 1, K[fork {e} ], e®2 ; σ ) → (® (® e 1, K[()], e®2, e; σ ) e 1, K[e], e®2 ; σ ) → (® (® e 1, K[e ′], e®2 ; σ ′) e 1, K[throw v to cont(K ′)], e®2 ; σ ) → (® (® e 1, K ′[v], e®2 ; σ ) Fig. 2. The thread-pool step relation. Contextual refinement/equivalence. A program e contextually refines a program e ′ if both pro- grams have type τ and no well-typed context (a closed top-level program with a hole) can distinguish a situation where e ′ is replaced by e. We write C : (Ξ | Γ; τ ) { (Ξ′ | Γ ′; τ ′) for a context (a term with a hole) such that Ξ′ | Γ ′ ⊢ C[e] : τ ′ holds whenever Ξ | Γ ⊢ e : τ does. We define contextual refinement of e ′ by e, written Ξ | Γ ⊢ e ≤ctx e ′ : τ , as follows: Ξ | Γ ⊢ e ≤ctx e ′ : τ ≜ Ξ | Γ ⊢ e : τ and Ξ | Γ ⊢ e ′ : τ and for any C such that C : (Ξ | Γ; τ ) { (· | ·; 1) holds C[e] ⇓ implies C[e ′] ⇓ where e ⇓ stands for termination of e when run under the empty heap defined as follows: e ⇓≜ ∃v, e®, σ . (e; ∅) →∗ (v, e®; σ ) Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:7 (e, σ ) → (e ′, σ ′) ((rec f(x) = e) v, σ ) →K (e[v, (rec f(x) = e)/x, f], σ ) (unfold (fold v), σ ) →K (v, σ ) ((Λ e) _, σ ) →K (e, σ ) (if true then e 2 else e 3, σ ) →K (e 2, σ ) (if false then e 2 else e 3, σ ) →K (e 3, σ ) (π 1 (v 1, v 2 ), σ ) →K (v 1, σ ) (π2 (v 1, v 2 ), σ ) →K (v 2, σ ) (match inj1 v with inj1 x ⇒ e 1 | inj2 x ⇒ e 2 end, σ ) →K (e 1 [v/x], σ ) (match inj2 v with inj1 x ⇒ e 1 | inj2 x ⇒ e 2 end, σ ) →K (e 2 [v/x], σ ) ℓ < dom(σ ) σ = σ ′ ⊎ {ℓ 7→ v ′ } v = σ (ℓ) (ref(v), σ ) →K (ℓ, σ ⊎ {ℓ 7→ v}) ′ (ℓ ← v, σ ) →K ((), σ ⊎ {ℓ 7→ v}) (! ℓ, σ ) →K (v, σ ) σ = σ ′ ⊎ {ℓ 7→ v} σ = σ ′ ⊎ {ℓ 7→ v ′′ } v , v ′′ (cas(ℓ, v, v ′), σ ) →K (true, σ ′ ⊎ {ℓ 7→ v ′ }) (cas(ℓ, v, v ′), σ ) →K (false, σ ) (call/cc (x . e), σ ) →K (e[cont(K)/x], σ ) Fig. 3. An excerpt of the head-reduction rules The intuitive explanation above for contextual refinement is the reason why in a contextual refinement e ≤ctx e ′ or in a logical relatedness relation e ≤log e ′, usually, the program on the left hand side, e, is referred to as the implementation side and the program on the right hand side, e ′, is referred to as the specification side. Two programs are contextually equivalent, if each contextually refines the other: Ξ | Γ ⊢ e ≈ctx e ′ : τ ≜ Ξ | Γ ⊢ e ≤ctx e ′ : τ ∧ Ξ | Γ ⊢ e ′ ≤ctx e : τ 3 LOGICAL RELATIONS It is challenging to construct logical relations for languages with higher-order store because of the so-called type-world circularity [Ahmed 2004; Ahmed et al. 2002; Birkedal et al. 2011]. The logic of Iris is rich enough to allow for a direct inductive specification of the logical relations for programming languages with advanced features such as higher-order references, recursive types, and concurrency [Krebbers et al. 2017b; Krogh-Jespersen et al. 2017; Timany et al. 2018]. 3.1 An Iris primer Iris [Jung et al. 2016; JUNG et al. 2018; Jung et al. 2015; Krebbers et al. 2017a] is a state-of-the-art higher-order concurrent separation logic designed for verification of programs. In Iris one can quantify over the Iris types κ: fin κ ::= 1 |κ × κ |κ → κ | Ectx | Var | Expr | Val | N | B |κ −⇀ κ | finset(κ) | Monoid | Names | iProp | . . . Here Ectx, Var, Expr and Val are Iris types for evaluation contexts, variables, expressions and µ,ref values of Fconc,cc . Natural numbers, N, and Booleans B are also included among the base types of fin Iris. Iris also features partial maps with finite support, κ −⇀ κ, and finite sets, finset(κ). Resources in Iris are represented using partial commutative monoids, Monoid, and instances of resources are Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:8 Amin Timany and Lars Birkedal named using so-called ghost-names, Names. Finally, and most importantly, there is a type of Iris propositions iProp. The grammar for Iris propositions is as follows: P ::= ⊤ | ⊥ | P ∗ P | P −∗ P | P ∧ P | P ⇒ P | P ∨ P | ∀x : κ. Φ(x) | ∃x : κ. Φ(x) N | ▷ P | µr .P | □ P | wp e x . P | {P } e {x . Q } | |⇛ P | P | . . . Here, ⊤, ⊥, ∧, ∨, ⇒, ∀, ∃ are the standard higher-order logic connectives. The predicates Φ are Iris predicates, i.e., terms of type κ → iProp. The connective ∗ is the separating conjunction. Intuitively, P ∗ Q holds if resources can be split into two disjoint pieces such that one satisfies P and the other Q. The magic wand connective P −∗ Q is satisfied by resources such that when these resources are combined with some resource satisfying P the resulting resources would satisfy Q. The ▷ modality, pronounced “later” is a modality that intuitively corresponds to some abstract form of step-indexing [Appel and McAllester 2001; Appel et al. 2007; Dreyer et al. 2011]. Intuitively, ▷ P holds if P holds one step into the future. Iris has support for taking fixed points of guarded propositions, µr .P. This fixed point can only be defined if all occurrences of r in P are guarded, i.e., appear under a ▷ modality. We use guarded fixed points for defining the interpretation of recursive µ,ref types in Fconc,cc . For any proposition P we have P ⊢ ▷ P. When the modality □ is applied to a proposition P, the non-duplicable resources in P are forgotten, and thus □ P is “persistent.” In general, we say that a proposition P is persistent if P ⊣⊢ □ P (where ⊣⊢ is the logical equivalence of Iris propositions). A key property of persistent propositions is that µ,ref they are duplicable: P ⊣⊢ P ∗ P. The type system of Fconc,cc is not a sub-structural type system and variables (in the typing environment) may be used multiple times. Therefore when we interpret types as logical relations in Iris, those relations should be duplicable. We use the persistence modality □ to ensure this. µ,ref The Iris program logic for Fconc,cc . Iris facilitates specification and verification of programs by means of weakest-preconditions wp e x . P , which intuitively hold whenever e is safe and, more- over, whenever e terminates with a resulting value v, then P[v/x] holds. When x does not appear in P we write wp e x . P as wp e P . Also, we sometimes write wp e Φ for wp e x . Φ(x) In Iris, Hoare triples are defined in terms of weakest preconditions: {P } e {x . Q } ≜ □ P −∗ wp e x . Q Note that the □ modality ensures that the Hoare triples are persistent and hence duplicable (in separation logic jargon, Hoare triples should just express “knowledge” and not claim ownership of any resources). A key feature of Iris (as for other concurrency logics) is that specification and verification is done thread-locally: the weakest precondition only describes properties of execution of a single thread. Concurrent interactions are abstracted and reasoned about in terms of resources (rather than by explicit reasoning about interleavings). For programming languages that do not include continuations or other forms of non-local control flow, the weakest precondition is not only thread-local, but also what we may call context-local. Context-local means that to reason about an expression in an evaluation context, it suffices to reason about the expression in isolation, and then separately about what the context does to the resulting value. This form of context-locality is formally expressed by the soundness of the following bind rule inadmissible-bind wp e x . wp K[x] Φ wp K[e] Φ Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:9 This rule is not sound when expressions include call/cc since call/cc captures the evaluation context and hence its behaviour depends on it. We discussed inadmissibility of this rule in Introduction. µ,ref Thus, for reasoning about Fconc,cc we cannot use the “standard” Iris rules [Jung et al. 2016; JUNG et al. 2018; Jung et al. 2015; Krebbers et al. 2017a,b] for weakest preconditions. Instead, we use new rules such as the following: fst-wp if-true-wp rec-wp ▷ wp K[v] Φ ▷ wp K[e] Φ ▷ wp K[e[rec f (x) = e, v/f , x]] Φ wp K[if true then e else e ′] Φ wp K[(rec f (x) = e) v] Φ wp K[π1 (v, w)] Φ callcc-wp throw-wp ▷ wp K[e[cont(K)/x]] Φ ▷ wp K ′[v] Φ wp K[call/cc (x . e)] Φ wp K[throw v to cont(K ′)] Φ The difference from the standard rules is that our new rules include an explicit context K. Earlier, such rules could be derived using the bind rule, but that is not sound in general in our settings. Note that the context is used in the rules callcc-wp and throw-wp for call/cc and throw. These two rules directly reflect the operational semantics of call/cc and throw. To demonstrate how the rules of our program logic are used to reason about a program we discuss the following program: call/cc (x . (throw 5 to x) + 4) + 2 This program first captures the current continuation, [ ] + 2, and then continues with evaluating the throw operation. At that point, the throw operation causes the program to forget about the rest of computation, i.e., adding 4 and 2, and jumps to the captured continuation, i.e., [ ] + 2, with value 5. Hence, the overall result is 7. We prove this fact, i.e., wp call/cc (x . (throw 5 to x) + 4) + 2 x . x = 7 , in our program logic as follows: trivial wp 5 + 2 x . x = 7 throw-wp with K = ([ ] + 4) + 2, and, K ′ = [ ] + 2 wp ((throw 5 to cont([ ] + 2)) + 4) + 2 x . x = 7 callcc-wp with K = [ ] + 2 wp call/cc (x . (throw 5 to x ) + 4) + 2 x . x = 7 Notice the importance of the context K in applying the rule callcc-wp in this proof. µ,ref In summa, for Fconc,cc we use new non-context-local rules for reasoning about weakest preconditions, and the non-context-local rules allow us to reason about call/cc and throw. Because of the explicit context K, the non-context-local rules for weakest preconditions are somewhat more elaborate to use than the corresponding context-local rules. However, that is the price we have to pay to be able to reason in general about non-local control flow. In Section 4 we will see how we can still recover a form of context-local weakest precondition for reasoning about those parts of the program that do not use non-local control flow. In the rules above for weakest preconditions, the antecedent is only required to hold a step of computation later (▷) — that is because these rules correspond to expressions performing a reduction step. The update modality and invariants. The update modality |⇛ accounts for updating (allocation, deallocation and mutation) of resources.1 Intuitively, |⇛ P is satisfied by resources that can be updated to new resources for which P holds. For any proposition P, we have that P ⊢ |⇛ P. If P holds, then resources can be updated (trivially) so as to have that P holds. The update modality is 1 This modality is called the fancy update modality in Krebbers et al. [2017a]. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:10 Amin Timany and Lars Birkedal idempotent, |⇛ |⇛ P ⊣⊢ |⇛ P. We write P ≡∗ Q as a shorthand for P −∗ |⇛Q. Crucially, resources can be updated throughout a proof of weakest preconditions: |⇛ wp e Φ ⊣⊢ wp e Φ ⊣⊢ wp e x . |⇛Φ(x) N N Iris features invariants P for enforcing concurrent protocols. Each invariant P has a name, N N , associated to it. Names are used to keep track of which invariants are open.2 Intuitively, P states that P always holds. The following rules govern invariants. inv-open-wp inv-alloc e is atomic ▷P N (▷ R) −∗ wp e y. (▷ R) ∗ wp K[y] x . Q R N wp K[e] x . Q |⇛ P These rules say that invariants can always be allocated by giving up the resources being protected by the invariant and they can be kept opened only during the execution of physically atomic opera- tions. Iris invariants are impredicative, i.e., they can state P holds invariantly for any proposition P, including invariants. This is why the later operator is used as a guard to avoid self-referential para- doxes [Krebbers et al. 2017a]. Invariants essentially express the knowledge that some proposition N N holds invariantly. Hence, invariants are always persistent, i.e., P ⊣⊢ □ P . 3.2 Resources used in defining logical relations We need some resources in order to define our logical relations in Iris. We need resources for repre- senting memory locations of the implementation side, the memory locations of the specification side and the expression being evaluated on the specification side. These resources are written as follows: – ℓ 7→i v: memory location ℓ contains value v on the implementation side. –ℓ→ 7 s v: memory location ℓ contains value v on the specification side. – j Z⇒ e: the thread j on the specification side is about to execute e. These resources are defined using more primitive resources in Iris, but we omit such details here. What is important is that we can use these resources to reason about programs. In particular, we can derive the following rules (and similarly for other basic expressions) for weakest preconditions and for execution on the specification side. ∀ℓ. ℓ 7→i v −∗ wp K[ℓ] Φ ℓ 7→i v −∗ wp K[v] Φ ▷ ℓ 7→i v wp K[! ℓ] Φ wp K[ref(v)] Φ ℓ 7→i w −∗ wp K[()] Φ ▷ ℓ 7→i v ℓ 7→s v j Z⇒ K[! ℓ] j Z⇒ K[ref(v)] |⇛ ∃ℓ. ℓ 7→s v ∗ j Z⇒ K[ℓ] |⇛ ℓ 7→s v ∗ j Z⇒ K[v] wp K[ℓ ← w] Φ ℓ 7→s v j Z⇒ K[ℓ ← w] |⇛ ℓ 7→s w ∗ j Z⇒ K[()] These resources are all exclusive in the sense that: ℓ 7→i v ∗ ℓ 7→i v ′ ⊢ ⊥ ℓ 7→s v ∗ ℓ 7→s v ′ ⊢ ⊥ j Z⇒ e ∗ j Z⇒ e ′ ⊢ ⊥ 2 Officially in Iris, the update modality is in fact annotated with so-called masks (sets of invariant names), which are used to ensure that invariants are not re-opened. For simplicity, we do not include masks in this paper. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:11 3.3 Logical relations in Iris µ,ref Figure 4 presents our binary logical relation for Fconc,cc . We define the logical relation in several stages. The first thing we define is the relation of observational refinement. Intuitively, an expression e observationally refines an expression e ′ if, whenever e reduces to a value so does e ′. We define this in Iris using magic wand and weakest precondition. The whole formula reads as follows: assuming that there is some thread j on the specification side that is about to execute e ′ (represented in Iris by j Z⇒ e ′) then, after execution of e, we know that thread j on the specification side has also been executed to some value w. We then use the notion of observational refinement defined above to define the value relation, the expression relation and the evaluation context relation for each type. In contrast to earlier definitions of logical relations in Iris [Krebbers et al. 2017b; Krogh-Jespersen et al. 2017; Timany et al. 2018], our logical relation is an example of so-called biorthogonal logical relations [Pitts 2005], also known as top-top closed logical relations. That is, we define two expressions to be related if plugging them into related evaluation contexts results in observationally related expressions. Two evaluation contexts are defined to be related if plugging related values into them results in observationally related expressions. The value relation interpretation JΞ ⊢ τ K∆ of a type τ in context Ξ is defined by induction on τ . Here ∆ is an environment mapping type variables in Ξ to Iris relations. For all the non-continuation types, the definition is exactly as in for the language without call/cc [Krebbers et al. 2017b]. Pairs of values of base types, 1, B, and N, are related if they are equal values of their corresponding type. A pair of values are related at the sum type if they are both formed by applying the same injection to values that are in turn related at the appropriate type. A pair of values are related at the product type, τ × τ ′, if they are each a pair of values such that their first components are related at τ and their second components are related at τ ′. The value interpretation of recursive types are defined using Iris’s guarded fixpoint operator µr .P. It intuitively states that two values of are related at a recursive types if they are both folded values with their underlying values again related at recursive types. The value relation for functions types τ → τ ′ expresses that two values of the function type are related if whenever applied to related values of the domain type, τ , the resulting expressions are related at the codomain type, τ ′. The use of the persistently modality, □, is to make sure that value interpretations of polymorphic programs are persistent. The value relation for polymorphic values requires two related values to produce two related expressions when instantiated, regardless of what predicate f we take as the interpretation of the type variable; provided that f is a persistent predicate. The use of the persistently modality here, as well as the side-condition on f being persistent, are required to ensure that the value interpretations are persistent. Two values of a reference type are related if they are both locations that always (expressed using Iris invariants) store related values. Finally, the relational interpretation of cont(τ ) expresses that two continuations are related whenever their corresponding evaluation contexts are related at the evaluation context relation for the type in question. The evaluation context relation KJΞ ⊢ τ K∆ relates evaluation contexts K and K ′ if plugging related values of type τ in them results in observationally related expressions. The expression relation is the standard biorthogonal expression relation. It states that EJΞ ⊢ τ K∆ (e, e ′) holds whenever, for any two related evaluation contexts K and K ′, the expressions K[e] and K ′[e ′] are observationally related. The notion of logical relatedness states, as usual for call-by-value languages, that two expressions e and e ′ are logically related if substituting related values for their free variables results in related expressions. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:12 Amin Timany and Lars Birkedal Observational refinement: O : Expr × Expr → iProp O(e, e ) ≜ ∀j. j Z⇒ e ′ −∗ wp e ∃w. j Z⇒ w ′ Value interpretation of types: JΞ ⊢ τ K∆ : Val × Val → iProp JΞ ⊢ αK∆ ≜ ∆(α) JΞ ⊢ 1K∆ (v, v ′) ≜ v = v ′ = () JΞ ⊢ BK∆ (v, v ′) ≜ v = v ′ = true ∨ v = v ′ = false JΞ ⊢ NK∆ (v, v ′) ≜ ∃n. v = v ′ = n Ü JΞ ⊢ τ1 + τ2 K∆ (v, v ′) ≜ (∃w, w ′ . v = inji w ∧ v ′ = inji w ′ ∧ JΞ ⊢ τi K∆ (w, w ′)) i ∈ {1,2} JΞ ⊢ τ × τ K∆ (v, v ) ≜ ∃w 1, w 2, w 1′ , w2′ . v = (w 1, w 2 ) ∧ v ′ = (w 1′ , w 2′ ) ∧ ′ ′ JΞ ⊢ τ K∆ (w 1, w 1′ ) ∗ JΞ ⊢ τ ′K∆ (w 2, w 2′ ) JΞ ⊢ µα . τ K∆ ≜ µ f : Val × Val → iProp. λ(v, v ′). ∃w, w ′ . v = fold w ∧ v ′ = fold w ′ ∧ ▷Jα, Ξ ⊢ τ K∆,α 7→f (w, w ′) JΞ ⊢ τ → τ ′K∆ (v, v ′) ≜ □ ∀w, w ′ . JΞ ⊢ τ K∆ (w, w ′) ⇒ EJΞ ⊢ τ ′K∆ (v w, v ′ w ′) JΞ ⊢ ∀α . τ K∆ (v, v ′) ≜ ∀f : Val × Val → iProp. persistent(f ) ⇒ □ EJα, Ξ ⊢ τ K∆,α 7→f (v _, v ′ _) JΞ ⊢ ref(τ )K∆ (v, v ′) ≜ ∃ℓ, ℓ ′ . v = ℓ ∧ v ′ = ℓ ′∧ N.ℓ.ℓ′ ∃w, w ′ . ℓ 7→i w ∗ ℓ ′ 7→s w ′ ∗ JΞ ⊢ τ K∆ (w, w ′) JΞ ⊢ cont(τ )K∆ (v, v ′) ≜ ∃K, K ′ . v = cont(K) ∧ v ′ = cont(K ′) ∧ KJΞ ⊢ τ K∆ (K, K ′) Evaluation context interpretation of types: KJΞ ⊢ τ K∆ : Ectx × Ectx → iProp KJΞ ⊢ τ K∆ (K, K ′) ≜ ∀v, v ′ . JΞ ⊢ τ K∆ (v, v ′) ⇒ O(K[v], K ′[v ′]) Expression interpretation of types: EJΞ ⊢ τ K∆ : Expr × Expr → iProp EJΞ ⊢ τ K∆ (e, e ′) ≜ ∀K, K ′ . KJΞ ⊢ τ K∆ (K, K ′) ⇒ O(K[e], K ′[e ′]) Logical relatedness: Ξ | Γ ⊨ e ≤log e ′ : τ : iProp for Γ = x 1 : τ1, . . . , x n : τn ∗ ! #» #»′ #»/ #» #» x ], e ′[v ′/ #» Ξ | Γ ⊨ e ≤log e : τ ≜ ∀∆, v , v . ′ JΞ ⊢ τi K∆ (vi , vi ) ⇒ EJΞ ⊢ τ K∆ e[ v ′ x] x i :τi The map ∆ : Var → (Val × Val) → iProp maps free type variables to their value interpretations. The λ in the definition of JΞ ⊢ µα . τ K∆ is the meta-level λ used for forming an Iris predicate. µ,ref Fig. 4. An excerpt of the logical relations for Fconc,cc Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:13 µ,ref We can now state and prove the fundamental theorem of logical relations for Fconc,cc . The theorem expresses that any well-typed expression is logically related to itself. Theorem 3.1 (Fundamental theorem of logical relations). Ξ | Γ ⊢ e : τ ⇒ Ξ | Γ ⊨ e ≤log e : τ This theorem is proven by induction on the typing derivation using the basic rules for weakest- preconditions and executions on the specification side. The above theorem, together with some basic properties of observational refinement, implies the soundness of our logical relations, i.e., that logical relatedness implies contextual refinement: Theorem 3.2 (Soundness of logical relations). Ξ | Γ ⊨ e ≤log e ′ : τ ⇒ Ξ | Γ ⊨ e ≤ctx e ′ : τ Our logical relation is expressed in terms of weakest preconditions and the proofs of the above theorems use the earlier presented proof rules for weakest preconditions. Before turning to ap- plications, we pause to present context-local weakest preconditions, which we can use to simplify reasoning about program fragments, which do not use non-local control flow. 4 CONTEXT-LOCAL WEAKEST PRECONDITIONS To make it simpler to reason about expressions that do not use non-local control flow, we define a new notion of context-local weakest precondition (CLWP). The definition is given in terms of the earlier weakest precondition, which, as we will explain below, means that we will be able to mix and match reasoning steps using (non-context local) weakest preconditions and context-local weakest preconditions. Definition 4.1. The context-local weakest precondition of e with respect to Φ is defined as follows: clwp e Φ ≜ ∀K, Ψ. (∀v. Φ(v) −∗ wp K[v] Ψ ) −∗ wp K[e] Ψ Based on this, we also define context-local Hoare triples: {P }cl e {x . Q } ≜ □ P −∗ clwp e x . Q Note how the above definition essentially says that clwp e Φ holds if the bind rule holds for e, which intuitively means that e behaves context-locally. Another way to look at thedefinition of context-local weakest preconditions above is the following. In order to prove clwp e Φ , we have to show that given any evaluation context K and predicate Ψ we have to show that running e under K can satisfy postcondition Ψ. Since K and Ψ are universally quantified and the only thing we know about them is that ∀v. Φ(v) −∗ wp K[v] Ψ , the only way for the program K[e] to guarantee Ψ as its postcondition is that it would, in its execution, eventually reach a point K[v] for a value v such that Φ(v). This means that intuitively e does not tamper with the evaluation context it is running under. In other words, for all intents and purposes e behaves context-locally. Therefore, the bind rule below is sound for context-local weakest preconditions. bind clwp e x . clwp K[x] Φ clwp K[e] Φ Moreover, the “standard” rules for the basic language constructs (excluding call/cc and throw, of course) can also be derived for context-local weakest preconditions, as shown in Figure 5. We Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:14 Amin Timany and Lars Birkedal fst-clwp if-true-clwp rec-clwp ▷ clwp v Φ ▷ clwp e Φ ▷ clwp e[v/x][rec f (x) = e/f ] Φ clwp if true then e else e ′ Φ clwp (rec f (x) = e) v Φ clwp π1 (v, w) Φ load-clwp alloc-clwp ▷ ℓ 7→i v clwp ref(v) x . ∃ℓ.x = ℓ ∗ ℓ 7→i v clwp ! ℓ x . x = v ∗ ℓ 7→i v Fig. 5. An excerpt of inference rules for CLWP’s. can also use invariants during atomic steps of computation while proving context-local weakest preconditions. inv-open-clwp N (▷ R) −∗ clwp e x . (▷ R) ∗ Q R e is atomic clwp e x . Q Now we have both (non-context-local) weakest preconditions and context-local weakest precon- ditions. What is the upshot of this? The key point is that when we prove correctness / relatedness of programs, we can use the simpler context-local weakest preconditions for reasoning about those parts of the program which are context local (do not use call/cc or throw) and only use the (non-context-local) weakest preconditions for reasoning about those parts that may involve non-local control flow. This fact is expressed formally by the rule clwp-wp below, which establishes a connection between weakest-preconditions and context-local weakest preconditions. clwp-wp clwp e Ψ ∀v. Ψ(v) −∗ wp K[v] Φ wp K[e] Φ This rule basically says that if we know that e context-locally guarantees postcondition Ψ then we can prove wp K[e] Φ by assuming that, locally under the context K, it will only evaluate to values that satisfy Ψ. Moreover, it guarantees that the evaluation of e does not tamper with the evaluation context that we are considering it under. It is easy to show that clwp e Φ implies wp e Φ ; simply take K to be the empty evaluation context, [ ], and Ψ to be Φ. Hence, similarly to a (non-context-local) weakest precondition, the context-local weakest precondition clwp e Φ also implies the safety of e, and, that whenever e terminates with a value v,Φ(v) holds. The proposition clwp e Φ only says that e behaves context-locally. Therefore, in principle, we should be able to give context-local specifications to programs that do use call/cc and throw, but still behave context-locally. For instance, the following example from Section 3.1: call/cc (x . (throw 5 to x) + 4) + 2 This program does indeed use call/cc and throw, but it does not tamper with the evaluation context that it runs under. That is to say that the effects of call/cc and throw are confined within the program itself. Hence, we can prove that the following context-local specification holds for this program. clwp call/cc (x . (throw 5 to x) + 4) + 2 x . x = 7 However, as there are no context-local reasoning rules for call/cc and throw, we have to unfold the definition of context-local weakest precondition proposition and prove this fact manually: Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:15 trivial (∀v . v = 7 −∗ wp K [v] Ψ ) ⊢ wp K [5 + 2] Ψ throw-wp (∀v . v = 7 −∗ wp K [v] Ψ ) ⊢ wp K [((throw 5 to cont(K [[ ] + 2])) + 4) + 2] Ψ callcc-wp (∀v . v = 7 −∗ wp K [v] Ψ ) ⊢ wp K [call/cc (x . (throw 5 to x ) + 4) + 2] Ψ introducing assumptions ∀K , Ψ. (∀v . v = 7 −∗ wp K [v] Ψ ) −∗ wp K [call/cc (x . (throw 5 to x ) + 4) + 2] Ψ unfolding clwp clwp call/cc (x . (throw 5 to x ) + 4) + 2 x . x = 7 5 WEB SERVER REFINEMENT The combination of continuations and concurrency allows for a simplified implementation of web servers. Such servers store explicitly captured (using call/cc) server-side continuations in order to track the state of communication with the client [Flatt 2017; Hendershott 2017; Krishnamurthi et al. 2007; Might 2017; Queinnec 2004]. To serve a returning user such web servers simply resume the stored continuation for that user. We refer to these servers as continuation-based as opposed to the more traditional state-storing, where server stores data that it later uses to reconstruct the state of the server for returning clients. In this section we show that two simple servers, one implemented in continuation-based style and one implemented in state-storing style, are equivalent. Two Servers. The two servers that we consider take a number as a request. They reply to each user with the sum of the numbers that that user has submitted. Figure 6 shows implementations of the handler functions of the servers.3 The handlers take a connection (of type serverConnT) as input which consists of a pair of functions for reading the request and writing the response. The idea is that these functions are an abstraction of a TCP connection and thus the contextual equivalence can be understood as showing that clients cannot distinguish between the two implementations. These servers both internally use a table to associate a resumption id (a number to remember the client by) to each client. Here the functions associate and get are used for storing into the table and looking up resumption ids in the table, respectively. The state-storing implementation associates to a resumption id the sum so far. The continuation-based implementation associates a captured continuation to a resumption id. Each returning client sends its resumption id along with its request. The function sumloop in the continuation based implementation is essentially a loop that sends the sum so far to the client and asks for the next number by calling read__client. The function read__client captures the current continuation and associates it with a resumption id. This resumption id is then sent to the client. After this, the server stops as the request in question is served.4 Notice that the read__client never returns. In practice the control is returned to the point after the call to this function when the client returns with the resumption id associated to the current continuation. In this case, as the connection is new, the server will supply the new connection (reader, writer) along with the new request. Since the two servers, apart from their handlers, are identical (they just pass requests to their handlers) we here only discuss the contextual equivalence of the two handlers by showing that each handler refines the other. Here we show one of these refinements: Ξ | Γ ⊨ handler2 ≤log handler1 : ServerConnT → 1 The other is similar. The two handlers internally use a concurrent (protected by a spin lock) table to store and look-up resumptions. The table and lock implementations are straightforward and thus omitted. Since these 3 We µ ,ref use an ML-like syntax for the sake of brevity and legibility; our Coq formalization includes the Fconc,cc code for these handlers. 4 The command abort is the command that ends the program (thread) and can be written in our programming language as throw () to [] where [] is the empty evaluation context. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

105:16 Amin Timany and Lars Birkedal (* In the code below, the function `resumptionid` converts the index of a continuation in the table into a session id, i.e., a session cookie. Similarly, the function `result` formats the response appropriately, making it ready to be sent to the client. *) 1 let handler1 : ServerConnT -> 1 = 2 let tb = newTable () in 3 fun (cn : ServerConnT) -> 4 let (reader, writer) = cn in 5 match reader () with 6 (Some cid, n) -> 7 begin 8 match get tb cid with 9 None -> () (* unknown resumption id! *) 10 | Some sum -> writer (result (sum + n)); 11 writer (resumptionid (associate tb (sum + n))); 12 abort 13 end 14 | (None, n) -> 15 writer (result n); 16 let cid = associate tb n in 17 writer (resumptionid cid) 1 let read__client tb writer = 2 callcc (k. writer (resumptionid (associate tb k)); abort) 3 4 let rec sumloop m reader writer = 5 writer (result m); 6 let (v, reader, writer) = read__client tb writer in 7 sumloop (m + v) reader writer 8 9 let handler2 : ServerConnT -> 1 = 10 let tb = newTable () in 11 fun (cn : ServerConnT) -> 12 let (reader, writer) = cn in 13 match reader () with 14 (Some cid, n)-> 15 begin 16 match get tb cid with 17 None -> () (*unknown resumption id!*) 18 | Some k -> throw (n,reader,writer) to k 19 end 20 | (None, n)-> sumloop n reader writer Fig. 6. Two server handlers: one state-storing (top) and one continuation-based (bottom). implementations do not use call/cc and throw, we give their relational specs using context-local weakest preconditions. Given the rule clwp-wp we can use these specs during the proof of contextual refinement of handlers. We discuss the relational specs of the table before presenting the refinement of handlers. 5.1 Relational spec for the table and the lock The essence of relating the tables on both sides (specification side and implementation side) is simple. Two tables are related if their contents are. For this purpose we introduce the predicate relTables(v, v ′, γ , Φ) which states that the table v is related to the table v ′ where their contents are related by the binary predicate Φ. We ignore γ for now. It is only used for the internal lock protecting the table. With this definition, new tables are related (as they are both empty). The related specs for the get and associate operations require that only related values can be stored Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

Mechanized Relational Verif. of Conc. Prog. with Continuations 105:17 into tables and guarantee that when looking the table up we are guaranteed to receive related values, if any. What does it mean for the contents, i.e., a number and a continuation to be related here, i.e., what should we take for Φ? The answer is simple. The number n is related to the continuation K if n is the same as the number that the suspended program in K considers to be the sum. Notice that this relation specifies some details about the program captured into K. This program uses the table itself! Therefore, it is not possible to write down the relation for the contents of the table before the table is created. As a result, the standard relational spec for the table, e.g., the relational spec that we get for free from the fundamental theorem of logical relations, does not suffice for our application. Such standard specs require the relation on the contents to be given before the table is created: ∀Φ. { j Z⇒ K[newTable ()]}cl (weaker standard spec) newTable () {x . ∃v ′ . j Z⇒ K[v ′] ∗ ∃γ . relTables(x, v ′, γ , Φ)} Note the quantification over Φ outside the whole triple. Hence, we give the following stronger relational spec to our tables: { j Z⇒ K[newTable ()]}cl newTable () {x . ∃v ′ . j Z⇒ K[v ′] ∗ ∀Φ. |⇛ ∃γ . relTables(x, v ′, γ , Φ)} {relTables(tb, tb ′, γ , Φ) ∗ j Z⇒ K[get tb ′ n]}cl get tb n x . ∃v ′ . j Z⇒ K[v ′] ∗ x = v ′ = None ∨ { (∃w, w ′ x = Some(w) ∧ v ′ = Some(w ′) ∗ Φ(v, v ′)) } {relTables(tb, tb ′, γ , Φ) ∗ Φ(v, v ′) ∗ j Z⇒ K[associate tb ′ v]}cl associate tb v {x . ∃n. x = n ∗ j Z⇒ K[n]} Notice that with our stronger specification we can refer to the tables themselves in the predicate Φ that we pick for relating the contents, whereas in the (weaker standard spec) specification one has to pick this relation beforehand, and hence one cannot refer to the tables v and v ′ because they have not been created yet! The predicate relTables(tb, tb ′, γ , Φ) is defined in terms of the relLocks predicate, which pertains to the relational specification of spin locks given below. relTables(tb, tb ′, γ , Φ) ≜ relLocks(tb.lock, tb ′ .lock, γ , PΦ ) PΦ ≜ ∃ls. contents(tb, map π 1 ls) ∗ contents(tb ′, map π2 ls) ∗ ∗ (x ,x ′ )∈ls Φ(x, x ′) Here tb.lock is the lock protecting the table tb. The proposition PΦ above simply states that the there is a list of pairs of values, which are pairwise related by Φ and, moreover, that the first projections of these pairs are stored in the implementation side table and the second projections of these pairs are stored in the specification side table. The contents predicate simply specifies that the index of an element in the table is its index in the list. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 105. Publication date: August 2019.

You can also read