Automated Synthesis of Asynchronizations

Asynchronous programming is widely adopted for building responsive and efficient software, and modern languages such as C# provide async/await primitives to simplify the use of asynchrony. In this paper, we propose an approach for refactoring a sequential program into an asynchronous program that uses async/await, called asynchronization. The refactoring process is parametrized by a set of methods to replace with asynchronous versions, and it is constrained to avoid introducing data races. We investigate the delay complexity of enumerating all data race free asynchronizations, which quantifies the delay between outputting two consecutive solutions. We show that this is polynomial time modulo an oracle for solving reachability in sequential programs. We also describe a pragmatic approach based on an interprocedural data-flow analysis with polynomial-time delay complexity. The latter approach has been implemented and evaluated on a number of non-trivial C# programs extracted from open-source repositories

Introduction
Asynchronous programming is widely adopted for building responsive and efficient software. As an alternative to explicitly registering callbacks with asynchronous calls, C# 5.0 [3] introduced the async/await primitives. These primitives allow the programmer to write code in a familiar sequential style without explicit callbacks. An asynchronous procedure, marked with async, returns a task object that the caller uses to "await" it. Awaiting may suspend the execution of the caller, but does not block the thread it is running on. The code after await is the continuation called back when the callee result is ready. This paradigm has become popular across many languages, C++, JavaScript, Python.
The async/await primitives introduce concurrency which is notoriously complex. The code in between a call and a matching await (referring to the same task) may execute before some part of the awaited task or after the awaited task finished. For instance, on the middle of Fig. 1, the assignment y=1 at line 4 can execute before or after RdFile finishes. The await for ReadToEndAsync in RdFile (line 13) may suspend RdFile's execution because ReadToEndAsync did not finish, and pass the control to Main which executes y=1. If ReadToEndAsync finishes before this await executes, then the latter has no effect and y=1 gets executed after RdFile finishes. The resemblance with sequential code can be especially deceitful since this non-determinism is opaque. It is common that awaits are placed immediately after the corresponding call which limits the benefits that can be obtained from executing steps in the caller and callee concurrently [25].
In this paper, we address the problem of writing efficient asynchronous code that uses async/await. We propose a procedure for automated synthesis of asynchronous programs equivalent to a given synchronous (sequential) program . This can be seen as a way of refactoring synchronous code to asynchronous code. Solving this problem in its full generality would require checking equivalence between arbitrary programs, which is known to be hard. Therefore, we consider a restricted space of asynchronous program candidates defined by substituting synchronous methods in with asynchronous versions (assumed to be behaviorally equivalent). The substituted methods are assumed to be leaves of the call-tree (they do not call any method in ). Such programs are called asynchronizations of . A practical instantiation is replacing IO synchronous calls for reading/writing files or managing http connections with asynchronous versions.
For instance, the sequential C# program on the left of Fig. 1 contains a Main that invokes a method RdFile that returns the length of the text in a file. The file name input to RdFile is an input to Main. The program uses a variable x to aggregate the lengths of all files accessed by RdFile; this would be more useful when Main calls RdFile multiple times which we omit for simplicity. Note that this program passes the assertion at line 7. The time consuming method Read-ToEnd for reading a file is an obvious choice for being replaced with an equivalent asynchronous version whose name is suffixed with Async. Performing such tasks asynchronously can lead to significant performance boosts. The program on the middle of Fig. 1 is an example of an asynchronization defined by this substitution. The syntax of async/await imposes that every method that transitively calls one of the substituted methods, i.e., Main and RdFile, must also be declared as asynchronous. Then, every asynchronous call must be followed by an await that specifies the control location where that task should have completed. For instance, the await for ReadToEndAsync is placed at line 13 since the next instruction (at line 14) uses the computed value. Therefore, synthesizing such refactoring reduces to finding a correct placement of awaits (that implies equivalence) for every call of a method that transitively calls a substituted method (we do not consider "deeper" refactoring like rewriting conditionals or loops).
We consider an equivalence relation between a synchronous program and an asynchronization that corresponds to absence of data races in the asynchronization. Data race free asynchronizations are called sound. Relying on absence of data races avoids reasoning about equality of sets of reachable states which is harder in general, and an established compromise in reasoning about concurrency. For instance, the asynchronization in Fig. 1 is sound because the call to RdFile accessing x finishes before the read of x in Main (line 6). Therefore, accesses to x are performed in the same order as in the synchronous program.
The asynchronization on the right of Fig. 1 is not the only sound (data-race free) asynchronization of the program on the left. The await at line 13 can be moved one statement up (before the read of x) and the resulting program remains equivalent to the sequential one. In this paper, we investigate the problem of enumerating all sound asynchronizations of a sequential program w.r.t. substituting a set of methods with asynchronous versions. This makes it possible to deal separately with the problem of choosing the best asynchronization in terms of performance based on some metric (e.g., performance tests).
Identifying the most efficient asynchronization is difficult and can not be done syntactically. It is tempting to consider that increasing the distance between calls and matching awaits so that more of the caller code is executed while waiting for an asynchronous task to finish increases performance. However, this is not true in general. We use the programs in Fig. 2 to show that the best await placement w.r.t. performance depends on execution times of code blocks in between calls and awaits in a non-trivial manner. Note that estimating these execution times, especially for IO operations like http connections, can not be done statically.
The programs in Fig. 2 use Thread.Sleep(n) to abstract sequential code executing in milliseconds and Task.Delay(n) to abstract an asynchronous call executing in milliseconds on a different thread. The functions named Foo differ only in the position of await t. We show that modifying this position worsens execution time in each case. For the left program, best performance corresponds to maximal distance between await t in Foo and the corresponding call. This allows the IO call to execute in parallel with the caller, as depicted on the bottomleft of Fig. 2. The executions corresponding to the other two positions of await t are given just above. For the middle program, placing await t in between the two code blocks in Foo optimizes performance (note the extra IO call in Main): the IO call in Foo executes in parallel with the first code block in Foo and the IO call in Main executes in parallel with the second one. This is depicted on the bottom-middle of Fig. 2. The execution above shows that placing await t as on   the left (after the two code blocks) leads to worse execution time (placing await t immediately after the call is also worse). Finally, for the right program, placing await t immediately after the call is best (note that IO executes another code block before await). The IO call in Main executes in parallel with Foo as shown on the bottom-right of Fig. 2. The execution above shows the case where await t is placed in the middle (the await has no effect because IO already finished, and Foo continues to execute). This leads to worse execution time (placing await t after the two code blocks is also worse). These differences in execution times have been confirmed by running the programs on a real machine. Fig. 2, the performance of an asynchronization depends on the execution environment, e.g., the overhead of IO operations like http connections and disk access (in Fig. 2, we use Thread.Sleep(n) or Task.Delay(n) to model such overheads). Since modeling the behavior of an execution environment w.r.t. performance is difficult in general, selecting the most performant asynchronization using static reasoning is also difficult. As a way of sidestepping this difficulty, we focus on enumerating all sound asynchro-nizations that allows to evaluate performance separately in a dynamic manner using performance tests for instance (for each sound asynchronization).

As demonstrated by the examples in
In the worst-case, the number of (sound) asynchronizations is exponential in the number of method calls in the program. Therefore, we focus on the delay complexity of the problem of enumerating sound asynchronizations, i.e., the complexity of the delay between outputting two consecutive (distinct) solutions, and show that this is polynomial time modulo an oracle for solving reachability (assertion checking) in sequential programs. Note that a trivial enumeration of all asynchronizations and checking equivalence for each one of them has an exponential delay complexity modulo an oracle for checking equivalence.
As an intermediate step, we consider the problem of computing maximal sound asynchronizations that maximize the distance between every call and its matching await. We show that rather surprisingly, there exists a unique maximal sound asynchronization. This is not trivial since asynchronizations can be incomparable w.r.t. distances between calls and awaits (i.e., better for one await and worse for another, and vice-versa). This holds even if maximality is relative to a given asynchronization imposing an upper bound on the distance between awaits and calls. In principle, avoiding data races could reduce to a choice between moving one await or another closer to the matching call. We show that this is not necessary because the maximal asynchronization is required to be equivalent to a sequential program, which executes statements in a fixed order.
As a more pragmatic approach, we define a procedure for computing sound asynchronizations which relies on a bottom-up interprocedural data-flow analysis. The placement of awaits is computed by traversing the call graph bottom up and using a data-flow analysis that computes read or write accesses made in the callees. We show that this procedure computes maximal sound asynchronizations of abstracted programs where every Boolean condition is replaced with non-deterministic choice. These asynchronizations are sound for the concrete programs as well. This procedure enables a polynomial-time delay enumeration of sound asynchronizations of abstracted programs.
We implemented the asynchronization enumeration based on data-flow analysis in a prototype tool for C# programs. We evaluated this implementation on a number of non-trivial programs extracted from open source repositories to show that our techniques have the potential to become the basis of refactoring tools that allow programmers to improve their usage of async/await primitives.
In summary, this paper makes the following contributions: -Define the problem of data race-free (sound) asynchronization synthesis for refactoring sequential code to equivalent asynchronous code (Section 3). -Show that the problem of computing a sound asynchronization that maximizes the distance between calls and awaits has a unique solution (Section 4). -The delay complexity of sound asynchronization synthesis (Sections 5-6).
-A pragmatic algorithm for computing sound asynchronizations based on a data-flow analysis (Section 7). -A prototype implementation of this algorithm and an evaluation of this prototype on a benchmark of non-trivial C# programs (Section 8). Additional formalization and proofs are included in the appendix.

Asynchronous Programs
We consider a simple programming language to formalize our approach, shown in Fig. 3. A program is a set of methods, including a distinguished main, which are classified as synchronous or asynchronous. Synchronous methods run continuously until completion when they are invoked. Asynchronous methods, marked using the keyword async, can run only partially and be interrupted when executing an await. Only asynchronous methods can use await, and all methods using await must be defined as asynchronous. We assume that methods are not (mutually) recursive. A program is called synchronous if it is a set of synchronous methods. A method is defined by a name from a set M and a list of statements over a set PV of program variables, which can be accessed from different methods (ranged over using , , ,. . .), and a set LV of method local variables (ranged over using , 1 , 2 ,. . .). Input/return parameters are modeled using program variables. Each method call returns a unique task identifier from a set T, used to record control dependencies imposed by awaits (for uniformity, synchronous methods return a task identifier as well). Our language includes assignments, awaits, returns, loops, and conditionals. Assignments to a local variable := , where is a program variable, are called reads of , and assignments to a program variable := ( is an expression over local variables) are called writes to . A base method is a method whose body does not contain method calls. Asynchronous methods. Asynchronous methods can use awaits to wait for the completion of a task (invocation) while the control is passed to their caller. The parameter of the await specifies the id of the awaited task. As a sound abstraction of awaiting the completion of an IO operation (reading or writing a file, an http request, etc.), which we do not model explicitly, we use a variation await *. This has a non-deterministic effect of either continuing to the next statement in the same method (as if the IO operation already completed), or passing the control to the caller (as if the IO operation is still pending).   Fig. 1. We use program variables to represent system resources such as the file system. The await for the completion of accesses to such resources is modeled by await *. This enables capturing racing accesses to system resources in asynchronous executions. Parameters or return values are modeled using program variables. ReadToEndAsync is modeled using reads/writes of the index/content of the input stream, and await * models the await for their completion.
We assume that the body of every asynchronous method satisfies several well-formedness syntactic constraints, defined on its control-flow graph (CFG). We recall that each node of the CFG represents a basic block of code (a maximallength sequence of branch-free code), and nodes are connected by directed edges which represent a possible transfer of control between blocks. Thus, 1. every call := call ′ uses a distinct variable (to store task identifiers), 2. every CFG block containing an await is dominated by the CFG block containing the call := call . . . (i.e., every CFG path from the entry to the await has to pass through the call), 3. every CFG path starting from a block containing a call := call . . . to the exit has to pass through an await statement. The first condition simplifies the technical exposition, while the last two ensure that stores a valid task identifier when executing an await , and that every asynchronous invocation is awaited before the caller finishes. Languages like C# or Javascript do not enforce the latter constraint, but it is considered bad practice due to possible exceptions that may arise in the invoked task and are not caught. We forbid passing task identifiers as method parameters (which is possible in C#). A statement await is said to match a statement := call ′ .

Semantics.
A program configuration is a tuple (g, stack, pend, cmpl, c-by, w-for) where g is composed of the valuation of the program variables excluding the program counter, stack is the call stack, pend is the set of asynchronous tasks, e.g., continuations predicated on the completion of some method call, cmpl is the set of completed tasks, c-by represents the relation between a method call and its caller, and w-for represents the control dependencies imposed by await statements. The activation frames in the call stack and the asynchronous tasks are represented using triples ( , , ℓ) where ∈ T is a task identifier, ∈ M is a method name, and ℓ is a valuation of local variables, including as usual a dedicated program counter. The set of completed tasks is represented as a function cmpl : T → {⊤, ⊥} such that cmpl( ) = ⊤ when is completed and cmpl( ) =⊥, otherwise. We define c-by and w-for as partial functions T ⇀ T with the meaning that c-by( ) = , resp., w-for( ) = , iff is called by , resp., is waiting for . We set w-for( ) = * if the task was interrupted because of an await * statement.
The semantics of a program is defined as a labeled transition system (LTS) [ ] = (C, Act, ps 0 , →) where C is the set of program configurations, Act is a set of transition labels called actions, ps 0 is the initial configuration, and →⊆ C × Act × C is the transition relation. Each program statement is interpreted as a transition in [ ]. The set of actions is defined by (Aid is a set of action identifiers): The transition relation → is defined in Fig. 6. Transition labels are written on top of →.
Transitions labeled by (aid , , rd( )) and (aid , , wr( )) represent a read and a write accesses to the program variable , respectively, executed by the task (method call) with identifier . A transition labeled by (aid , , call( )) corresponds to the fact that task executes a method call that results in creating a task . Task is added on the top of the stack of currently executing tasks, declared pending (setting cmpl( ) to ⊥), and c-by is updated to track its caller (c-by( ) = ). A transition (aid , , return) represents the return from task . Task is removed from the stack of currently executing tasks, and cmpl( ) is set to ⊤ to record the fact that task is finished. A transition (aid , , await( )) relates to task waiting asynchronously for task . Its effect depends on whether task is already completed. If this is the case (i.e., cmpl[ ] = ⊤), task continues and executes the next statement. Otherwise, task executing the await is removed from the stack and added to the set of pending tasks, and w-for is updated to track the waiting-for relationship (w-for( ) = ). Similarly, a transition (aid , , await(*)) corresponds to task waiting asynchronously for the completion of an unspecified task. Nondeterministically, task continues to the next statement, or task is interrupted and transferred to the set of pending tasks (w-for( ) is set to *).
A transition (aid , , cont) represents the scheduling of the continuation of task . There are two cases depending on whether waited for the completion of another task modeled explicitly in the language (i.e., w-for( ) = ), or an unspecified task (i.e., w-for( ) = *). In the first case, the transition is enabled only when the call stack is empty and is completed. In the second case, the transition is always enabled. The latter models the fact that methods implementing IO operations (waiting for unspecified tasks in our language) are executed in background threads and can interleave with the main thread (that executes the Main method). Although this may seem restricted because we do not allow arbitrary interleavings between IO methods and Main, this is actually sound when focusing on the existence of data races as in our approach. As shown later in Table 1, any two instructions that follow an await * are not happens-before related and form a race.
By the definition of →, every action a ∈ Act ∖ {( , , cont)} corresponds to executing some statement in the program, which is denoted by S( ). r := x ∈ inst(ℓ(pc)) aid ∈ Aid fresh ℓ ′ = ℓ[ ↦ → g( ), pc ↦ → next(ℓ(pc))] (g, ( , , ℓ) ∘ stack, , , , ) aid ∈ Aid fresh w-for( ) = * The function inst returns the instruction at some given control location while next gives the next instruction to execute. We use ∘ to denote sequence concatenation and init to denote the initial state of a method call.
An execution of is a sequence = ps 0 a1 − → ps 1 a2 − → . . . of transitions starting in the initial configuration ps 0 and leading to a configuration ps where the call stack and the set of pending tasks are empty. C[ ] denotes the set of all program variable valuations included in configurations that are reached in executions of . Since we are only interested in reasoning about the sequence of actions a 1 ·a 2 ·. . . labeling the transitions of an execution, we will call the latter an execution as well. The set of executions of a program is denoted by Ex( ).
Traces. The trace of an execution ∈ Ex( ) is a tuple tr( ) = ( , MO, CO, SO, HB) of strict partial orders between the actions in defined in Table 1. The method invocation order MO records the order between actions in the same invocation, and the call order CO is an extension of MO that additionally orders actions before an invocation with respect to those inside that invocation. The synchronous happens-before order SO orders the actions in an execution as if all the invocations were synchronous (even if the execution may contain asynchronous ones).
It is an extension of CO where additionally, every action inside a callee is ordered before the actions following its invocation in the caller. The (asynchronous) happens-before order HB contains typical control-flow constraints: it is an extension of CO where every action inside an asynchronous invocation is ordered before the corresponding await in the caller, and before the actions following its invocation in the caller if precedes the first 5 await in MO (an invocation can be interrupted only when executing an await) or if the callee does not contain an await (it is synchronous). Tr( ) is the set of traces of . Table 1: Strict partial orders included in a trace. CO, SO, and HB are the smallest satisfying relations.
a1 occurs before a2 in and a1 ̸ = a2 a1 ∼ a2 a1 = ( , , ) and a2 = ( , , ) On the right of Fig. 1, we show a trace where two statements (represented by the corresponding lines numbers) are linked by a dotted arrow if the corresponding actions are related by MO, a dashed arrow if the corresponding actions are related by CO but not by MO, and a solid arrow if the corresponding actions are related by the HB but not by CO.

Synthesizing Asynchronous Programs
Given a synchronous program and a subset of base methods ⊆ , our goal is to synthesize all asynchronous programs that are equivalent to and that are obtained by substituting every method in with an equivalent asynchronous version. The base methods are considered to be models of standard library calls (e.g., IO operations) and asynchronous versions are defined by inserting await * statements in their body. We use [ ] to emphasize a subset of base methods in a program . Also, we call a library. A library is called (a)synchronous when all methods are (a)synchronous. Asynchronizations of a synchronous program. Let [ ] be a synchronous program, and a set of asynchronous methods obtained from those in by inserting at least one await * statement in their body (and adding the keyword async). Each method in corresponds to a method in with the same name, and vice-versa.
[ ] is called an asynchronization of [ ] with respect to if it is a syntactically correct program obtained by replacing the methods in with those in and adding await statements as necessary.  More precisely, let * ⊆ be the set of all methods of that transitively call methods of . Formally, * is the smallest set of methods that includes and satisfies the following: if a method calls ′ ∈ * , then ∈ * . Then, [ ] is an if it is obtained from as follows: -Each method in is replaced with the corresponding method from .
-All methods in * ∖ are declared as asynchronous (because every call to an asynchronous method is followed by an await and any method using await must be asynchronous). -For each invocation := call of ∈ * , add await statements await satisfying the well-formedness syntactic constraints described in Section 2. Problem definition. We investigate the problem of enumerating all asynchronizations of a given program w.r.t. a given asynchronous library, which are sound, in the sense that they do not admit data races. Two actions a 1 and a 2 in a trace = ( , MO, CO, SO, HB) are concurrent if (a 1 , a 2 ) ̸ ∈ HB and (a 2 , a 1 ) ̸ ∈ HB. An ansynchronous program admits a data race (a 1 , a 2 ), where (a 1 , a 2 ) ∈ SO, if a 1 and a 2 are two concurrent actions of a trace ∈ Tr( ), and a 1 and a 2 are read or write accesses to the same program variable , and at least one of them is a write. We write data races as ordered pairs w.r.t. SO to simplify the definition of the algorithms in the next sections. Also, note that traces of synchronous programs can not contain concurrent actions, and therefore they do not admit data races. strongAsy[ , , ] does not admit data races as well.
[ ] is called sound when it does not admit data races. The absence of data races implies equivalence to the original program, in the sense of reaching the same set of configurations (program variable valuations).

Enumerating Sound Asynchronizations
We present an algorithm for solving asynchronization synthesis, which relies on a partial order between asynchronizations that guides the enumeration of possible solutions. The partial order takes into account the distance between calls and corresponding awaits. Fig. 8 pictures the partial order for asynchronizations of the program on the left of Fig. 1. Each asynchronization is written as a vector of distances, the first (second) element is the number of statements between await t1 (await t) and the matching call (we count only statements that appear in the sequential program). The edges connect comparable elements, smaller elements being below bigger elements. The asynchronization on the middle of Fig. 1 corresponds to the vector (1, 1). The highlighted elements constitute the set of all sound asynchronizations. The strong asynchronization corresponds to the vector (0, 0).
Formally, an await statement s in a method of an asynchronization [ ] ∈ Asy[ , , ] covers a read/write statement s in if there exists a path in the CFG of from the call statement matching s to s that contains s. The set of statements covered by an await s is denoted by Cover(s ). We compare asynchronizations in terms of sets of statements covered by awaits that match the same call from the synchronous program [ ]. Since asynchronizations are obtained by adding awaits, every call in asynchronization [ ] ∈ Asy[ , , ] corresponds to a fixed call in [ ]. Therefore, for two asynchronizations , ′ ∈ Asy[ , , ], is smaller than ′ , denoted by ≤ ′ , iff for every await s in , there exists an await s ′ in ′ that matches the same call as s , such that Cover(s ) ⊆ Cover(s ′ ). For example, the two asynchronous programs in Fig. 7 are ordered by ≤ since Cover(await 1) = {} in the first and Cover(await 1) = {r2 = x} in the second. Note that the strong asynchronization is smaller than every other asynchronization. Also, note that ≤ has a unique maximal element that is called the weakest asynchronization and denoted by wkAsy[ , , ]. In Fig. 8, the weakest asynchronization corresponds to the vector (2, 1).
In the following, we say moving an await down (resp., up) when moving the await further away from (resp. closer to) the matching call while preserving wellformedness conditions in Section 2. Further away or closer to means increasing or decreasing the set of statements that are covered by the await. For instance, if an await s in a program is preceded by a while loop, then moving it up means moving it before the whole loop and not inside the loop body. Otherwise, the third well-formedness condition would be violated. Relative Maximality. A crucial property of this partial order is that for every asynchronization , there exists a unique maximal asynchronization that is smaller than and that is sound. Formally, an asynchronization ′ is called a maximal asynchronization of relative to Lemma 1. Given an asynchronization ∈ Asy[ , , ], there exists a unique program ′ that is a maximal asynchronization of relative to .
Algorithm 1 An algorithm for enumerating all sound asynchronizations (these asynchronizations are obtained as a result of the output instruction). MaxRel returns the maximal asynchronization of relative to ← ImPred( ′ , s ); 5: for each ( ′′ , s ′′ ) ∈ 6: AsySyn( ′′ , s ′′ ); The asynchronization ′ exists because the bottom element of ≤ is sound. To prove uniqueness, assume by contradiction that there exist two incomparable maximal asynchronizations 1 and 2 and select the first await s 1 w.r.t. the control-flow of the sequential program that is placed in different positions in the two programs. Assume that s 1 is closer to its matching call in 1 . Then, we move s 1 in 1 further away from its matching call to the same position as in 2 . This modification does not introduce data races since 2 is data race free. Thus, the resulting program is data race free, bigger than 1 , and smaller than w.r.t. ≤ contradicting the fact that 1 is a maximal asynchronization.

Enumeration Algorithm
Our algorithm for enumerating all sound asynchronizations is given in Algorithm 1 as a recursive procedure AsySyn that we describe in two phases. First, ignore the second argument of AsySyn (in blue), which represents an await statement. For an asynchronization , AsySyn outputs all sound asynchronizations that are smaller than . It uses MaxRel to compute the maximal asynchronization ′ of relative to , and then, calls itself recursively for all immediate predecessors of ′ . AsySyn outputs all sound asynchronizations of when given as input the weakest asynchronization of . Recursive calls on immediate predecessors are necessary because the set of sound asynchronizations is not downward-closed w.r.t. ≤. For instance, the asynchronization on the right of Fig. 9 is an immediate predecessor of the sound asynchronization on the left but it has a data race on .
The delay complexity of this algorithm remains exponential in general, since a sound asynchronization may be outputted multiple times. Asynchronizations are only partially ordered by ≤ and different chains of recursive calls starting in different immediate predecessors may end up outputting the same solution. For instance, for the asynchronizations in Fig. 8, the asynchronization (0, 0) will be outputted twice because it is an immediate predecessor of both (1, 0) and (0, 1).
To avoid this redundancy, we use a refinement of the above that restricts the set of immediate predecessors available for a (recursive) call of AsySyn. This is based on a strict total order ≺ between awaits in a program that follows a topological ordering of its inter-procedural CFG, i.e., if s occurs before s ′ in the body of a method , then s ≺ s ′ , and if s occurs in a method and s ′ occurs in a method ′ s.t.
(indirectly) calls ′ , then s ≺ s ′ . Therefore, AsySyn takes an await statement s as a second parameter, which is initially the maximal element w.r.t. ≺ , and it calls itself only on immediate predecessors of a solution obtained by moving up an await s ′′ smaller than or equal to s w.r.t. ≺ . The recursive call on that predecessor will receive as input s ′′ . Formally, this relies on a function ImPred that returns pairs of immediate predecessors and await statements defined as follows: and s ′′ ⪯ s and ′′ ∈ ′ ↑ s ′′ } ( ′ ↑ s ′′ is the set of asynchronizations obtained from ′ by changing only the position of s ′′ , moving it up w.r.t. the position in ′ ). For instance, looking at immediate predecessors of (1, 1) in Fig. 8, (0, 1) is obtained by moving the first await in ≺ . Therefore, the recursive call on (0, 1) computes the maximal asynchronization relative to (0, 1), which is (0, 1), and stops (ImPred returns ∅ because the input s is the minimal element of ≺ , and already immediately after the call). Its immediate predecessor is explored when recursing on (1, 0). Algorithm 1 outputs all sound asynchronizations because after having computed a maximal asynchronization ′ in a recursive call with parameter s , any smaller sound asynchronization is smaller than some predecessor in ImPred( ′ , s ). Also, it can not output the same asynchonization twice. Let 1 and 2 be two predecessors in ImPred( ′ , s ) obtained by moving up the awaits s 1 and s 2 , respectively, and assume that s 1 ≺ s 2 . Then, all solutions computed in the recursive call on 1 will have s 2 placed as in ′ while all the solutions computed in the recursive call on 2 will have s 2 closer to the matching call. Therefore, the sets of solutions computed in these two recursion branches are distinct. The delay complexity of Algorithm 1 is polynomial time modulo an oracle that returns a maximal asynchronization relative to a given one. In the next section, we show that the latter problem can be reduced in polynomial time to the reachability problem in sequential programs.

Computing Maximal Asynchronizations
In this section, we present an implementation of the procedure MaxRel that relies on a reachability oracle. In particular, we first describe an approach for computing the maximal asynchronization relative to a given asynchronization , which can be seen as a way of repairing so that it becomes data-race free. Intuitively, we repeatedly eliminate data races in by moving certain await statements closer to the matching calls. The data races in (if any) are enumerated in a certain order that prioritizes data races between actions that occur first in executions of the original synchronous program. This order allows to avoid superfluous repair steps.

Data Race Ordering
An action a representing a read/write access in a trace of an asynchronization of is synchronously reachable if there is an action a ′ in a trace ′ of that represents the same statement, i.e., S(a) = S(a ′ ). It can be proved that any trace of an asynchronization contains a data race if it contains a data race between two synchronously reachable actions (see Appendix C). In the following, we focus on data races between actions that are synchronously reachable.
We define an order between such data races based on the order between actions in executions of the original synchronous program . This order relates data races in possibly different executions or asynchronizations of , which is possible because each action in a data race corresponds to a statement in .
For two read/write statements s and s ′ , s ≺ s ′ denotes the fact that there is an execution of in which the first time s is executed occurs before the first time s ′ is executed. For two actions a and a ′ in an execution/trace of an asynchronization, generated by two read/write statements s = S( ) and s ′ = S( ′ ), a ≺ SO a ′ holds if s ≺ s ′ and either s ′ ̸ ≺ s or s ′ is reachable from s in the interprocedural 6 control-flow graph of without taking any back edge 7 . For a deterministic synchronous program (admitting a single execution), a ≺ SO a ′ iff S( ) ≺ S( ′ ). For non-deterministic programs, when S( ) and S( ′ ) are contained in a loop body, it is possible that S( ) ≺ S( ′ ) and S( ′ ) ≺ S( ). In this case, we use the control-flow order to break the tie between a and a ′ .
The order between data races corresponds to the colexicographic order induced by ≺ SO . This is a partial order since actions may originate from different control-flow paths and are incomparable w.r.t. ≺ SO . Definition 2 (Data Race Order). Given two races (a 1 , a 2 ) and (a 3 , a 4 ) admitted by (possibly different) asynchronizations of a synchronous program , we have that (a 1 , a 2 ) ≺ SO (a 3 , a 4 ) iff a 2 ≺ SO a 4 , or a 2 = a 4 and a 1 ≺ SO a 3 .
Repairing a minimal data race (a 1 , a 2 ) w.r.t. ≺ SO removes any other data race (a 1 , a 4 ) with (a 2 , a 4 ) ∈ HB (note that we cannot have (a 4 , a 2 ) ̸ ∈ HB since a 2 ≺ SO a 4 ). The repair will enforce that (a 1 , a 2 ) ∈ HB which implies that (a 1 , a 4 ) ∈ HB.

Repairing Data Races
Repairing a data race (a 1 , a 2 ) reduces to modifying the position of a certain await. We consider only repairs where awaits are moved up (closer to the matching call). The "completeness" of this set of repairs follows from the particular order in which we enumerate data races.
Algorithm 2 The procedure MaxRel to find the maximal asynchronization of relative to . Let s 1 and s 2 be the statements generating a 1 and a 2 . In general, there exists a method that (transitively) calls another asynchronous method 1 that contains s 1 and before awaiting for 1 it (transitively) calls a method 2 that executes s 2 . This is pictured in Fig. 10. It is also possible that itself contains s 2 (see the program on the right of Fig. 7). The repair consists in moving the await for 1 before the call to 2 since this implies that s 1 will always execute before s 2 (and the corresponding actions are related by happens-before).
Formally, any two racing actions have a common ancestor in the call order CO which is a call action. The least common ancestor of a 1 and a 2 in CO among call actions is denoted by LCA CO (a 1 , a 2 ). In Fig. 10, it corresponds to the call statement s . More precisely, LCA CO (a 1 , a 2 ) is a call action a = ( , , call( )) s.t. (a , a 1 ) ∈ CO, (a , a 2 ) ∈ CO, and for each other call action a ′ , if (a , a ′ ) ∈ CO then (a ′ , a 1 ) ̸ ∈ CO. This call action represents an asynchronous call for which the matching await s must move to repair the data race. The await should be moved before the last statement in the same method generating an action which precedes a 2 in the reflexive closure of call order (statement s in Fig. 10). This way every statement that follows s in call order will be executed before s and before any statement which succeeds s in call order, including s 2 . Note that moving the await s anywhere after s will not affect the concurrency between a 1 and a 2 .
The pair (s , s) is called the root cause of the data race ( 1 , 2 ). Let RDR( , s , s) be the maximal asynchronization ′ smaller than w.r.t. ≤, s.t. no await statement matching s occurs after s on a CFG path.

A Procedure for Computing Maximal Asynchronizations
Given an asynchronization , the procedure MaxRel in Algorithm 2 computes the maximal asynchronization relative to by repairing data races iteratively until the program becomes data race free. The sub-procedure RCMinDR( ′ ) computes the root cause of a minimal data race (a 1 , a 2 ) of ′ w.r.t. ≺ SO such that the two actions are synchronously reachable. If ′ is data race free, RCMinDR( ′ ) returns ⊥. The following theorem states the correctness of MaxRel.
MaxRel( ) repairs a number of data races which is linear in the size of the input. Indeed, each repair results in moving an await closer to the matching call and before at least one more statement from the original program .
The problem of computing root causes of minimal data races is reducible to reachability (assertion checking) in sequential programs. This reduction builds on a program instrumentation for checking if there exists a data race that involves two given statements (s 1 , s 2 ) that are reachable in an executions of .This instrumentation is used in an iterative process where pairs of statements are enumerated according to the colexicographic order induced by ≺. For lack of space, we present only the main ideas of the instrumentation (see Appendix D). The instrumentation simulates executions of an asynchronization using nondeterministic synchronous code where methods may be only partially executed (modeling await interruptions). Immediately after executing s 1 , the current invocation 1 is interrupted (by executing a return added by the instrumentation). The active invocations that transitively called 1 are also interrupted when reaching an await for an invocation in this call chain (the other invocations are executed until completion as in the synchronous semantics). When reaching s 2 , if s 1 has already been executed and at least one invocation has been interrupted, which means that s 1 is concurrent with s 2 , then the instrumentation stops with an assertion violation. The instrumentation also computes the root cause of the data race using additional variables for tracking call dependencies.

Asymptotic Complexity of Asynchronization Synthesis
We state the complexity of the asynchronization synthesis problem. Algorithm 1 shows that the delay complexity of this problem is polynomial-time in the number of statements in input program modulo the complexity of computing a maximal asynchronization, which Algorithm 2 shows to be polynomial-time reducible to reachability in sequential programs. Since the reachability problem is PSPACE-complete for finite-state sequential programs [16], we get the following: Theorem 3. The output complexity 8 and delay complexity of the asynchronization synthesis problem is polynomial time modulo an oracle for reachability in sequential programs, and PSPACE for finite-state programs.
This result is optimal, i.e., checking whether there exists a sound asynchronization which is different from the trivial strong synchronization is PSPACEhard (follows from a reduction from the reachability problem). See Appendices D and E for the detailed formal proofs.

Asynchronization Synthesis Using Data-Flow Analysis
In this section, we present a refinement of Algorithm 2 that relies on a bottomup inter-procedural data flow analysis. The analysis is used to compute maximal asynchronizations for abstractions of programs where every Boolean condition (in if-then-else or while statements) is replaced with the non-deterministic choice *, and used as an implementation of MaxRel in Algorithm 1.
For a program , we define an abstraction # where every conditional if Besides adding the non-deterministic choice *, loops are unrolled exactly once. Every asynchronization of corresponds to an abstraction # obtained by applying exactly the same rewriting. # is a sound abstraction of in terms of sound asynchronizations it admits. Unrolling loops once is sound because every asynchronous call in a loop iteration should be awaited for in the same iteration (see the syntactic constraints in Section 2).
, then is a sound asynchronization of w.r.t. .
The procedure for computing maximal asynchronizations of # relative to a given asynchronization # traverses methods of # in a bottom-up fashion, detects data races using summaries of read/write accesses computed using a straightforward data-flow analysis, and repairs data races using the schema presented in Section 5.2. Applying this procedure to a real programming language requires an alias analysis to detect statements that may access the same memory location (this is trivial in our language which is used to simplify the exposition).
We consider an enumeration of methods called bottom-up order, which is the reverse of a topological ordering of the call graph 9 . For each method , let ℛ( ) be the set of program variables that can read, which is defined as the union of ℛ( ′ ) for every method ′ called by and the set of program variables read in statements in the body of . The set of variables ( ) that can write is defined in a similar manner. We define RW-var( ) = (ℛ( ), ( )). can do and that can be concurrent with accesses that a caller of can do after calling . These correspond to read/write statements that follow an await in , or to accesses in CRW-var( ′ ) for a method ′ called by . These sets of accesses can be computed using the following data-flow analysis: for all methods ∈ # in bottom-up order, and for each statement s in the body of from begin to end, if s is a call to ′ and s is not reachable from an await in the CFG of • CRW-var( ) ← CRW-var( ) ∪ CRW-var( ′ ) if s is reachable from an await statement in the CFG of • CRW-var( ) ← CRW-var( ) ∪ RW-var(s) We use (ℛ 1 , 1 ) ◁▷ (ℛ 2 , 2 ) to denote the fact that 1 ∩ (ℛ 2 ∪ 2 ) ̸ = ∅ or for all methods ∈ # in bottom-up order, and for each statement s in the body of from begin to end, • if s occurs between := call ′ and await (for some ′ ), and RW-var(s) ◁▷ CRW-var( ′ ), then # ← RDR( # , := call ′ , ) return # Theorem 5. MaxRel # ( # ) returns a maximal asynchronization relative to # .
Since MaxRel # is based on a single bottom-up traversal of the call graph of the input asynchronization # we get the following result.
Theorem 6. The delay complexity of the asynchronization synthesis problem restricted to abstracted programs # is polynomial time.

Experimental Evaluation
We present an empirical evaluation of our asynchronization synthesis approach, where maximal asynchronizations are computed using the data-flow analysis in Section 7. Our benchmark consists mostly of asynchronous C# programs from open-source GitHub projects. We evaluate the effectiveness in reproducing the original program as an asynchronization of a program where asynchronous calls are reverted to synchronous calls, along with other sound asynchronizations. Implementation. We developed a prototype tool that uses the Roslyn .NET compiler platform [27] to construct CFGs for methods in a C# program. This prototype supports C# programs written in static single assignment (SSA) form that include basic conditional/looping constructs and async/await as concurrency primitives. Note that object fields are interpreted as program variables in the terminology of §2 (data races concern accesses to object fields). It assumes that alias information is provided apriori; these constraints can be removed in the future with more engineering effort. In general, our synthesis procedure is compatible with any sound alias analysis. The precision of this analysis impacts only the set (number) of asynchronizations outputted by the procedure (a more precise analysis may lead to more sound asynchronizations).
The tool takes as input a possibly asynchronous program, and a mapping between synchronous and asynchronous variations of base methods in this program. It reverts every asynchronous call to a synchronous call, and it enumerates sound asynchronizations of the obtained program (using Algorithm 1). Table 2, which contains 5 synthetic examples (variations of the program in Fig. 1), 9 programs extracted from open-source C# GitHub projects (their name is a prefix of the repository name), and 2 programs inspired by questions on stackoverflow.com about async/await in C# (their name ends in Stackoverflow). Overall, there are 13 base methods involved in computing asynchronizations of these programs (having both synchronous and asynchronous versions), coming from 5 C# libraries (System.IO, System.Net, Windows.Storage, Microsoft.WindowsAzure.-Storage, and Microsoft.Azure.Devices). They are modeled as described in Section 2. Table 2: Empirical results. Syntactic characteristics of input programs: lines of code (loc), number of methods (m), number of method calls (c), number of asynchronous calls (ac), number of awaits that could be placed at least one statement away from the matching call (await # ). Data concerning the enumeration of asynchronizations: number of awaits that were placed at least one statement away from the matching call (await), number of races discovered and repaired (races), number of statements that the awaits in the maximal asynchronization are covering more than in the input program (cover), number of computed asynchronizations (async), and running time (t). Evaluation. The last five columns of Table 2 list data concerning the application of our tool. The column async lists the number of outputted sound asynchronizations. In general, the number of asynchronizations depends on the number of invocations (column ac) and the size of the code blocks between an invocation and the instruction using its return value (column await # gives the number of non-empty blocks). The number of sound asynchronizations depends roughly, on how many of these code blocks are racing with the method body. These asynchronizations contain awaits that are at a non-zero distance from the matching call (non-zero values in column await) and for many Github programs, this distance is bigger than in the original program (non-zero values in column cover). This shows that we are able to increase the distances between awaits and their matching calls for those programs. The distance between awaits and matching calls in maximal asynchronizations of non synthetic benchmarks is 1.27 statements on average. A statement representing a method call is counted as one independently of the method's body size. With a single level of inlining, the number of statements becomes 2.82 on average. However, these statements are again, mostly IO calls (access to network or disk) or library calls (string/bytes formatting methods) whose execution time is not negligible. The running times for the last three synthetic benchmarks show that our procedure is scalable when programs have a large number of sound asynchronizations.

Benchmark. Our evaluation uses a benchmark listed in
With few exceptions, each program admits multiple sound asynchronizations (values in column async bigger than one), which makes the focus on the delay complexity relevant. This leaves the possibility of making a choice based on other criteria, e.g., performance metrics. As shown by the examples in Fig. 2, their performance can be derived only dynamically (by executing them). These results show that our techniques have the potential of becoming the basis of a refactoring tool allowing programmers to improve their usage of the async/await primitives. The artifacts are available in a GitHub repository [2].

Related Work
There are many works on synthesizing or repairing concurrent programs in the standard multi-threading model, e.g., automatic parallelization in compilers [1,6,19], or synchronization synthesis [10,11,12,24,31,30,5,9,18]. We focus on the use of async/await which poses specific challenges that are not covered in these works.
Our semantics without await * instructions is equivalent to the semantics defined in [3,28]. But, to simplify the exposition, we consider a more restricted programming language. For the modeling of asynchronous IO operations, we follow [3] with the restriction that the code following an await * is executed atomically. This is sound when focusing on data-race freedom because even if executed atomically, any two instructions from different asynchronous IO operations (following await *) are not happens-before related. Program Refactoring. Program refactoring tools have been proposed for converting C# programs using explicit callbacks into async/await programs [25] or Android programs using AsyncTask into programs that use IntentService [22]. The C# tool [25], which is the closest to our work, makes it possible to repair misusage of async/await that might result in deadlocks. This tool cannot modify procedure calls to be asynchronous as in our work. A static analysis based technique for refactoring JavaScript programs is proposed in [17]. As opposed to our work, this refactoring technique is unsound in general. It requires that programmers review the refactoring for correctness, which is error-prone. Also, in comparison to [17], we carry a formal study of the more general problem of finding all sound asynchronizations and investigate its complexity. Data Race Detection. Many works study dynamic data race detection using happens-before and lock-set analysis, or timing-based detection [21,20,29,26,14]. They could be used to approximate our reduction from data race checking to reachability in sequential programs. Some works [4,23,13] propose static analyses for finding data races. [4] designs a compositional data race detector for multithreaded Java programs, based on an inter-procedural analysis assuming that any two public methods can execute in parallel. Similar to [28], they precompute method summaries to extract potential racy accesses. These approaches are similar to the analysis in Section 7, but they concern a different programming model. Analyzing Asynchronous Programs. Several works propose program analyses for various classes of asynchronous programs. [7,15] give complexity results for the reachability problem, and [28] proposes a static analysis for deadlock detection in C# programs that use both asynchronous and synchronous wait primitives. [8] investigates the problem of checking whether Java UI asynchronous programs have the same set of behaviors as sequential programs where roughly, asynchronous tasks are executed synchronously.

Conclusion
We proposed a framework for refactoring sequential programs to equivalent asynchronous programs based on async/await. We determined precise complexity bounds for the problem of computing all sound asynchronizations. This problem makes it possible to compute a sound asynchronization that maximizes performance by separating concerns -enumerate sound asynchronizations and evaluate performance separately. On the practical side, we have introduced an approximated synthesis procedure based on data-flow analysis that we implemented and evaluated on a benchmark of non-trivial C# programs.
The asynchronous programs rely exclusively on async/await and are deadlockfree by definition. Deadlocks can occur in a mix of async/await with "explicit" multi-threading that includes blocking wait primitives. Extending our approach for such programs is an interesting direction for future work.

A Formalization and Proofs of Section 3
The following lemma shows that the absence of data races implies equivalence to the original program, in the sense of reaching the same set of configurations (program variable valuations).

Lemma 2.
[ ] is sound implies Proof (Proof of Lemma 2). Let be an execution of that reaches a configuration ps ∈ C[ ]. We show that actions in can be reordered such that any action that occurs in between ( , , call( )) and ( , , return) is not of the form ( , , ) (i.e., the task is executed synchronously). If an action ( , , ) occurs in between ( , , call( )) and ( , , return), then it must be concurrent with ( , return). Since does not admit data races, an execution ′ resulting from by reordering any two concurrent actions reaches the same configuration ps as . Therefore, there exists an execution ′′ where the actions that occur between any ( , , call( )) and ( , , return) are not of the form ( , , ). This is also an execution of (modulo removing the awaits which have no effect), which implies ps ∈ C[ ].

B Formalization and Proofs of Section 4
The following lemma shows that for a given there exists a unique ′ that is a maximal asynchronization of relative to . The existence is implied by the fact that strongAsy[ , , ] is the bottom element of ≤. To prove uniqueness, we assume by contradiction that there exist two incomparable maximal asynchronizations 1 and 2 and select the first await statement s 1 , according to the control-flow of the sequential program, that is placed in different positions in the two programs. Assume that s 1 is closer to its matching call in 1 . Then, we move s 1 in 1 further away from its matching call to the same position as in 2 . This modification does not introduce data races since 2 is data race free. Thus, the resulting program is data race free, bigger than 1 , and smaller than w.r.t. ≤ contradicting the fact that 1 is a maximal asynchronization.
Lemma 3. Given an asynchronization ∈ Asy[ , , ], there exists a unique program ′ that is a maximal asynchronization of relative to .
Proof (Proof of Lemma 3). Since strongAsy[ , , ] is the bottom element of ≤, then there always exists a sound asynchronization smaller than . Assume by contradiction that there exist two distinct programs 1 and 2 that are both maximal asynchronizations of relative to . Let 1 (resp., 2 ) be an execution of 1 (resp., 2 ) where every await * does not suspend the execution of the current task, i.e., 1 and 2 simulate the synchronous execution of . Let s 1 be the statement corresponding to the first await action in 1 such that (1) there exists an await action in 2 with the corresponding await statement s 2 , such that s 1 and s 2 match the same call in , and Cover(s 1 ) ⊂ Cover(s 2 ) (this holds because 1 and 2 are distinct asynchronizations of the same synchronous program, thus Cover(s 1 ) and Cover(s 2 ) must be comparable), and (2) for every other await statement s 3 in 1 that generates an await action which occurs before the await action of s 1 in 1 , there exists an await statement s 4 in 2 matching the same call in , such that Cover(s 3 ) = Cover(s 4 ).
Let 3 be the program obtained from 1 by moving the await s 1 down (further away from the matching call) such that Cover(s 1 ) = Cover(s 2 ). Moving an await down can only create data races between actions that occur after the execution of the matching call. Then, 3 contains a data race iff there exists an execution of 3 and two concurrent actions a 1 and a 2 that occur between the action ( , , await( )) generated by s 1 and the action ( , , call( )) of the call matching s 1 , such that: (( , , call( )), a 1 ) ∈ CO, (a 1 , a ) ̸ ∈ HB, (( , , call( )), a 2 ) ∈ CO and (a 2 , ( , , await( ))) ∈ HB where the action a corresponds to the first await action in the task . Let s be the statement corresponding to the action a . Since the only difference between 3 and 2 is the placement of awaits then (( , , call( )), a 1 ) ∈ CO and (( , , call( )), a 2 ) ∈ CO hold in any execution ′ of 2 that contains the actions a 1 and a 2 . Also, note that since a occurs in the task that the action of s 1 is waiting for. This implies that in 1 the action of s occurs before the action of s 1 in 1 . Therefore, by the definition of s 1 we have that s in 1 covers the same set of statements as the corresponding s ′ in 2 that matches the same call as s . Consequently, (a 1 , a ′ ) ̸ ∈ HB and (a 2 , ( , , await( ))) ∈ HB hold in any execution ′ of 2 that contains the actions a 1 and a 2 (a ′ is the action of s ′ ). Thus, there exists an execution ′ of 2 such that the actions a 1 and a 2 are concurrent. This implies that if 3 admits a data race, then 2 admits a data race between actions generated by the same statements. As 2 is data race free, we get that 3 is data race free as well. Since 1 < 3 , we get that 1 is not maximal, which contradicts the hypothesis.
The complexity analysis also relies on a property of the maximal asynchronization relative to an immediate predecessor: if the predecessor is defined by moving an await s ′′ , then the maximal asynchronization is obtained by moving only awaits smaller than s ′′ w.r.t. ≺ .

Lemma 4.
If ′′ is an immediate predecessor of a sound asynchronization ′ , which is defined by moving an await s ′′ in ′ up, then the maximal sound asynchronization relative to ′′ is obtained by moving only awaits smaller than s ′′ w.r.t. ≺ .
Proof (Proof of Lemma 4). Moving an await up in ′ can only create data races between actions that occur after the execution of this await (because the invocation is suspended earlier). The only possible repairs of these data races consists in either moving s ′′ down which results in ′ or moving up some other awaits that occur in methods that (indirectly) call the method in which s ′′ occurs. The first case is not applicable because it gives a program that is not smaller than ′′ . In the second case, every await s ′ that is moved up occurs in a method that (indirectly) calls the method in which s ′′ occurs, and therefore, s ′ is smaller than s ′′ w.r.t. ≺ .
Before giving the proof of Theorem 1, we note that the total order relation ≺ between awaits is fixed throughout the recursion of AsySyn and it corresponds to the order of the awaits in the weakest asynchronization of , i.e., wkAsy[ , , ]. This is because the order between awaits in the same method might change from one asynchronization to another in Asy[ , , ]. If the control-flow graph of a method contains branches, it is possible to replace all await statements matching s that are reachable in the CFG from s with a single await statement s , in this case s is ordered before any other await that one of the awaits that s replaces is ordered before and is ordered after any await that all the awaits that s replaces are ordered before. Also, it is possible to add additional awaits statements in branches, in this case derive a total order between these awaits and order the awaits before or after any other await that the original await was ordered before or after, respectively.
Proof (Proof of Theorem 1). Let be the weakest asynchronization of , then the set of all sound asynchronizations of is = { ′′ : C[ ′′ ] = C[ ] and ′′ ≤ ′ }, where ′ is the maximal asynchronization of relative to . It is clear that every asynchronization outputted by AsySyn( , s 0 ) is in the set .
1 ′′ (resp., 2 ′′ ) is outputted by AsySyn( 1 ′ , s 1 ) (resp., AsySyn( 2 ′ , s 2 )), we have that the two programs are distinct since in 2 ′′ the await s 1 is in the same position as in ′ . Thus, we get that AsySyn outputs every element of only once.  The following lemma proves that for any unsound asynchronization, any trace with a data race contains at least one data race that involves two actions that are synchronously reachable. For instance, the program in Fig. 11 has two data races, one between = 1 and 4 = and the other between = 2 and 5 = . However, the statement = 2 is not reachable in the corresponding synchronous program. It is reachable in this asynchronization because of the data race between = 1 and 4 = , which are both reachable in the synchronous program. Eliminating the latter data race by moving the statement await 1 before = 1, makes = 2 unreachable and the data race between = 2 and 5 = is also eliminated.

Lemma 5. An asynchronization
[ ] is sound iff it does not admit data races between actions that are synchronously reachable.

Proof (Proof of Lemma 5). Assume by contradiction that
[ ] is sound and it admits a data race (a 1 , a 2 ) in a trace ∈ Tr( [ ]) where one of the actions, say a 1 , is not synchronously reachable. We assume w.l.o.g that the data race (a 1 , a 2 ) is the first that occurs in with at least one synchronously unreachable action. Then, there must exist a read access a that enabled a 1 , and therefore, a reads a value that was not read in any synchronous execution. Thus, the read value must the result of another data race that occurs earlier in the trace , which is a contradiction.  In Fig. 12, we explain how the repairing data races based on the partial order relating data races allows to avoid superfluous repair steps. For instance, in Fig. 12, the first data race to repair involves the read of x from Main and the write to x in m, because these statements are the first to execute in the original sequential program among the other statements involved in data races. Repairing this data race consists in moving await r1 before the read of x from Main, which implies that m completes before the read of x. This repair is defined from a notion of root cause of a data race, that in this case, contains the call to m and the read of x from Main. Interestingly, this repair step removes the write-write data race between the write to x in Main and the write to x in m as well. If we would have repaired these data races in the opposite order, we would have moved await t1 first before the write to x, and then, before the read of x. In Fig. 13, we give a non-deterministic program where two statements of the program can be executed in different orders in different executions. In particular, the statements r1 = x and r2 = y of the program can be executed in different orders depending on the number of loop iterations and whether the if branch is entered during the first loop iteration.  For the program in Fig. 14, we have the following order between data races: (x = input, r2 = x) ≺ SO (retVal = x, x = r2 + 1) because r2 = x is executed before the write x = r2 + 1 in the original synchronous program (for simplicity we use statements instead of actions). However, the data races (x = input, r2 = x) and (x = input, r3 = x) are incomparable.
The following lemma identifies a sufficient transformation for repairing a data race (a 1 , a 2 ): moving the await s generating the action a just before the statement s generating a. This is sufficient because it ensures that every statement that follows LCA CO (a 1 , a 2 ) 10 in call order will be executed before a and before any statement which succeeds a in call order, including a 2 . Note that moving the await a anywhere after a will not affect the concurrency between a 1 and a 2 . Lemma 6. Let (a 1 , a 2 ) be a data race in a trace of an asynchronization , and a = ( , call( )) = LCA CO (a 1 , a 2 ). Then, contains a unique action a = ( , await( )) and a unique action a such that: -(a, a ) ∈ MO, and a is the latest action in the method order MO such that (a , a) ∈ MO and (a, a 2 ) ∈ CO * (CO * denotes the reflexive closure of CO).
Proof (Proof of Lemma 6). Let be the execution of the trace . By definition, ends with a configuration where the call stack and the set of pending tasks are empty. Therefore, contains an action a = ( , , await( )) matching which is unique by the definition of the semantics. Since (a , a 1 ) ∈ CO and (a , a 2 ) ∈ CO then either a and a 2 occur in the same method, or there exists a call action a ′ in the same task as a such that (a ′ , a 2 ) ∈ CO. Then, we define a = a 2 in the first case, and a as the latest action in the same task as a such that (a, a 2 ) ∈ CO in the second case. We have that (a, a ) ∈ MO because otherwise, (a , a) ∈ MO and (a, a 2 ) ∈ CO * implies that (a 1 , a 2 ) ∈ HB (because (a 1 , a ) ∈ HB, and MO and CO are included in HB), and this contradicts a 1 and a 2 being concurrent.
When the control-flow graph of the method contains branches, the construction of RDR( , s , s) involves (1) replacing all await statements matching s that are reachable in the CFG from s with a single await statement placed just before s, and (2) adding additional await statements in branches that "conflict" with the branch containing s. This is to ensure the syntactic constraints described in Section 2. These additional await statements are at maximal distance from the corresponding call statement because of the maximality requirement.  For instance, to repair the data race between r2 = x and x = input in the program on the left of Fig. 15, the statement await r1 must be moved before r2 = x in the if branch, which implies that another await must be added on the else branch. The result is given on the right of Fig. 15.
The following lemma shows that repairing a minimal data race cannot introduce smaller data races (w.r.t. ≺ SO ), which ensures some form of monotonicity when repairing minimal data races iteratively.

Lemma 7.
Let be an asynchronization, (a 1 , a 2 ) a data race in that is minimal w.r.t. ≺ SO , and (s , s) the root cause of (a 1 , a 2 ). Then, RDR( , s , s) does not admit a data race that is smaller than (a 1 , a 2 ) w.r.t. ≺ SO . Proof of Lemma 7. The only modification in the program ′ = RDR( , s , s) compared to is the movement of the await s matching the call s to be before the statement s in a method . The concurrency added in ′ that was not possible in is between actions (a ′ , a ′′ ) generated by statements s ′ and s ′′ , respectively, as shown in Fig. 16. W.l.o.g., we assume that (a ′ , a ′′ ) ∈ SO. The statements s 1 and s 2 are those generating a 1 and a 2 , respectively. The statement s ′ is related by CO * to some statement in that follows s, and s ′′ is related by CO * to some statement that follows the call to in the caller of . Note that s ′ is ordered by ≺ after s 2 . Since (a 1 , a 2 ) ∈ SO and (a ′ , a ′′ ) ∈ SO then s 2 ≺ s ′′ and s 1 ≺ s ′ . Thus, any new data race (a ′ , a ′′ ) in ′ that was not reachable in is bigger than (a 1 , a 2 ).
Proof (Proof of Theorem 7). Since the recursive calls RCMinDR find all data races between synchronously reachable actions then the output ′ = MaxRel( ) is sound and therefore it is equivalent to (Lemma 2 and Lemma 5). Now we need to show that any successor 1 of ′ that is also smaller than (w.r.t. ≤) admits data races. Let s be the biggest await statement w.r.t. ≺ whose position in 1 is changed with respect to its position in ′ (moved down). Since 1 ≤ , then s was also moved up by the procedure MaxRel with respect to its position in to fix some data race (a 1 , a 2 ). Let be the method that contains s and s be the matching call. We will now show that (a 1 , a 2 ) forms a data race in 1 as well. 1 has an execution that reaches both a 1 and a 2 (since Ex( 1 ) includes the synchronous execution where all await * are interpreted as skip which reaches a 1 and a 2 ). Since every other await s ′ in 1 that occurs in a method ′ (in)directly called by (including the method associated with the call s ) is in the same position as in ′ , then the two actions a 1 and a 2 are not related by HB and are concurrent. Thus, (a 1 , a 2 ) forms a data race in 1 , which concludes the proof.
The fact that data races are enumerated in the order defined by ≺ SO guarantees a bound on the number of times an await matching the same call is moved during the execution of MaxRel( ). In general, this bound is the number of statements covered by all the awaits matching the call in the input program . Actually, this is a rather coarse bound. A more refined analysis has to take into account the number of branches in the CFGs. For programs without conditionals or loops, every await is moved at most once during the execution of MaxRel( ). In the presence of branches, a call to an asynchronous method may match multiple await statements (one for each CFG path starting from the call), and the data races that these await statements may create may be incomparable w.r.t. ≺ SO . Therefore, for a call statement s , let |s | be the sum of |Cover(s )| for every await s matching s in . Proof (Proof of Lemma 8). We consider first the case without conditionals or loops, and we show by contradiction that every await statement s is moved at most once during the execution of MaxRel( ), i.e., there exists at most one iteration of the while loop which changes the position of s . Suppose that the contrary holds for an await s . Let (a 1 , a 2 ), and (a 3 , a 4 ) be the data races repaired by the first and second moves of s , respectively. By Lemma 6, there exist two actions a and a ′ such that (a , a) ∈ MO, (a, a 2 ) ∈ CO * , (a, a ) ∈ MO and (a , a ′ ) ∈ MO, (a ′ , a 4 ) ∈ CO * , (a ′ , a ) ∈ MO where a = ( , , await( )) and a = ( , , call( )) are the asynchronous call action and the matching await action. Let s 2 and s 4 be the statements generating the two actions a 2 and a 4 , respectively. Then, we have either s 2 ≺ s 4 or s 2 = s 4 , and both cases imply that (a, a ′ ) ∈ MO * . Thus, moving the await statement generating a before the statement generating a implies that it is also placed before the statement generating a ′ (that occurs after a in the same method). Thus, the first move of the await s repaired both data races, which is contradiction.
In the presence of conditionals or loops, moving an await up in one branch may correspond to adding multiple awaits in the other conflicting branches. Also, one call in the program may correspond to multiple awaits on different branches. However, every repair of a data race consists in moving one await closer to the matching call s and before one more statement covered by some await matching s in the input .

D Computing Root Causes of Minimal Data Races
We present a reduction from the problem of computing root causes of minimal data races to reachability (assertion checking) in sequential programs. This reduction builds on a program instrumentation for checking if there exists a minimal data race that involves two given statements (s 1 , s 2 ) that are reachable in an execution of the original synchronous program, whose correctness relies on the assumption that another pair of statements cannot produce a smaller data race. This instrumentation is used in an iterative process where pairs of statements are enumerated according to the colexicographic order induced by ≺. This specific enumeration ensures that the assumption made for the correctness of the instrumentation is satisfied. Given an asynchronization , the instrumentation described in Fig. 17 represents a synchronous program where all await statements are replaced with synchronous code (lines [14][15][16][17][18][19][20]. This instrumentation simulates asynchronous executions of where methods may be only partially executed, modeling await interruptions. It reaches an error state (see the assert at line 10) when an action generated by s 1 is concurrent with an action generated by s 2 , which represents a data race, provided that s 1 and s 2 access a common program variable (these statements are assumed to be given as input). Also, the values of s and s when reaching the assertion violation represent the root-cause of this data race.
The instrumentation simulates an execution of to search for a data race as follows (we discuss the identification of the root-cause afterwards): -It executes under the synchronous semantics until an instance of s 1 is nondeterministically chosen as a candidate for the first action in the data race (s 1 can execute multiple times if it is included in a loop for instance). The current invocation is interrupted when it is about to execute this instance of s 1 and its task id 0 is stored into lastTaskDelayed (see lines 2-5). -Every invocation that transitively called 0 is interrupted when an await for an invocation in this call chain (whose task id is stored into lastTaskDelayed) would have been executed in the asynchronization (see line 18). -Every other method invocation is executed until completion as in the synchronous semantics. -When reaching s 2 , if s 1 has already been executed (lastTaskDelayed is not ⊥) and at least one invocation has only partially been executed, which is recorded in the boolean flag DescendantDidAwait and which means that s 1 is concurrent with s 2 , then the instrumentation stops with an assertion violation. A subtle point is that the instrumentation may execute code that follows an await even if the task has been executed only partially, which would not happen in an execution of the original . Here, we rely on the assumption that there exist no data race between that code and the rest of the task . Such data races would necessarily involve two statements which are before s 2 w.r.t. ≺. Therefore, the instrumentation is correct only if it is applied by enumerating pairs of statements (s 1 , s 2 ) w.r.t. the colexicographic order induced by ≺.
Next, we describe the computation of the root-cause, i.e., the updates on the variables s and s. By definition, the statement s in the root-cause should be a call that makes an invocation that is in the call stack when s 1 is reached. This can be checked using the variable lastTaskDelayed that stores the id of the last such invocation popped from the call stack (see the test at line 27). The statement s in the root-cause can be any call statement that has been executed in the same task as s (see the test at line 23), or s 2 itself (see line 9).
Let [[ , s 1 , s 2 ]] denote the instrumentation in Fig. 17. We say that the values of s and s when reaching the assertion violation are the root cause computed by this instrumentation. The following theorem states its correctness. Based on Theorem 8, we define an implementation of the procedure RCMinDR( ) used in computing maximal asynchronizations (Algorithm 2) as follows: -For all pairs of read or write statements (s 1 , s 2 ) in colexicographic order w.r.t.
≺ that are reachable in an execution of the original synchronous program .
• If [[ , s 1 , s 2 ]] reaches an assertion violation, then * return the root cause computed by [[ , s 1 , s 2 ]] return ⊥ Checking whether read or write statements are reachable can be determined using a linear number of reachability queries in the synchronous program . Also, the order ≺ between read or write statements can be computed using a quadratic number of reachability queries in the synchronous program . Therefore, s ≺ s ′ iff an instrumentation of that sets a flag when executing s and asserts that this flag is not set when executing s ′ reaches an assertion violation. The following theorem states the correctness of the procedure above.
Theorem 9. RCMinDR( ) returns the root cause of a minimal data race of w.r.t. ≺ SO , or ⊥ if ′ is data race free.

E Formalization and Proofs of Section 6
Theorem 10. Checking whether there exists a sound asynchronization different from the strong asynchronization is PSPACE-complete.
(1) define a new method that writes to a new program variable , and insert a call to followed by a write to at location ℓ, and (2) insert a write to after every call statement that calls a method in { ′ } * , where ′ is the method containing ℓ. Let be an asynchronous version of obtained by inserting an await * at the beginning. Then, ℓ is reachable in iff the only sound asynchronization of ′ w.r.t. { } is the strong asynchronization.

F Formalization and Proofs of Section 7
The MaxRel # procedure repairs data races in an order which is ≺ SO with some exceptions that do not affect optimality, i.e., the number of times an await matching the same call can be moved. For instance, if a method calls two other methods 1 and 2 in this order, the procedure above may handle 2 before 1 , i.e., repair data races between actions that originate from 2 before data races that originate from 1 , although the former are bigger than the latter in ≺ SO . This does not affect optimality because those repairs are "independent", i.e., any repair in 2 cannot influence a repair in 1 , and vice-versa. The crucial point is that this procedure repairs data races between actions that originate from a method before data races that involve actions in methods preceding in the call graph, which are bigger in ≺ SO than the former.
Note that MaxRel # procedure which is based on the bottom-up interprocedural data-flow analysis compromises precision to reduce the complexity of the problem from undecidable in general or PSPACE-complete with finite data to polynomial time. However, because of this imprecision, certain await statements may be moved closer to the matching call unnecessarily. For instance, in Fig. 11, the precise algorithm (using the procedure MaxRel in Algorithm 2) will only repair the data race on because doing so, the potential data race on will become unreachable. On the other hand, the polynomial-time algorithm (using the MaxRel # procedure) will also repair the data race on , moving another await closer to the matching call, since it cannot reason about data (one statement of this data race is only reachable if the variable 4 is 1).

G Multi-threaded Refactorings
We discuss an extension of our framework to multi-threaded refactorings that rewrite a sequential program into a multi-threaded program where every method invocation is executed on a different thread. A caller can wait for a callee to complete using a join primitive. A start primitive for spawning a new thread is the counterpart of an asynchronous call while join is the counterpart of await. For instance, Fig. 18 lists a sequential program, a possible asynchonization, and a multi-thread refactoring (both refactorings place the awaits/joins as far away as possible from the calls).
An important difference between start/join and async/await is the happensbefore order relation. For instance, the asynchronization on the center of Fig. 18 assigns 1 to x (line 11) before it assigns 2 to x (line 4), as in the original sequential program. However, the multi-thread program on the right of Fig. 18 may execute these two assignments in any order, and admits a behavior that is not possible in the sequential program (assigning 2 before assigning 1). Repairing this datarace consists in moving the join at line 5 to occur before assigning 2 to x at line 4. In general, the happens-before order is weaker compared to an analogous asynchronization, where awaits are placed as the joins, which implies that any multi-threaded refactoring can be rewritten to an asynchronization. The viceversa may not be possible as shown in this example.
Despite this difference, it can still be proved that there exists a unique multithreaded refactoring that is sound, i.e., does not admit data races, and maximal, i.e., maximizes the distance between start and join, a result similar to Lemma 3. Assuming by contradiction the existence of two incomparable maximal and sound refactorings, one can show that moving a join in one refactoring further away from the matching call as in the other refactoring does not introduce data races (contradicting optimality). To compute maximal and sound multi-threaded refactorings, one can apply the same iterative process of repairing data-races (the happens-before reflects multi-threading instead of async/await), prioritizing data races involving statements that would execute first in the sequential program. The repairing of a data-race is similar and consists in moving a join up.
In contrast to async/await, moving a join up does not introduce new data races (since no new parallelism is introduced). This implies that all the predecessors of a sound multi-threaded refactoring are also sound, i.e., the set of sound multi-threaded refactorings is downward closed.