Skip to content

Commit

Permalink
feat: implement async*/await* for efficient async abstraction (#3609
Browse files Browse the repository at this point in the history 
)

Add opt-in support for efficient abstraction of asynchronous code using `async*`/`await*` to delineate possible commits/context switches. Fixes #1482 and addresses https://forum.dfinity.org/t/canister-output-message-queue-limits-and-ic-management-canister-throttling-limits/15972/22.

Syntax:

```
<type ::= ...
  async* <typ>                                  delayed, asynchronous computation

<exp> ::= ...
  async* <block-or-exp>                          delay an asynchronous computation
  await* <block-or-exp>                          await a delayed computation (only in async)
```

This is another take on the design, avoid some of the pitfalls (but also advantages) of #3573 which proposed an eager `do async <block_or_exp>` but no new types.


## Async* types

`async* <typ>` specifies a delayed, asynchronous computation producing a value of type `<typ>`.

Computation types typically appear as the result type of a `local` function that produces an `await*`-able value.

(They cannot be used as the return types of `shared` functions.)

## Async*

The async expression `async* <block-or-exp>` has type `async* T` provided:

-   `<block-or-exp>` has type `T`;

-   `T` is shared.

Any control-flow label in scope for `async* <block-or-exp>` is not in scope for `<block-or-exp>`. However, `<block-or-exp>` may declare and use its own, local, labels.

The implicit return type in `<block-or-exp>` is `T`. That is, the return expression, `<exp0>`, (implicit or explicit) to any enclosed `return <exp0>?` expression, must have type `T`.

Evaluation of `async* <block-or-exp>` produces a delayed computation to evaluate `<block-or-exp>`. It immediately returns a value of type `async* T`.
The delayed computation can be executed using `await*`, producing one evaluation
of the computation `<block-or-exp>`.

### Danger

Note that `async <block-or-exp>` has the effect of scheduling a single asynchronous computation of `<exp>`, regardless of whether its result, a future, is consumed with an `await`.
Moreover, each additional consumption by an `await` just returns the previous result, without repeating the computation.

In comparison, `async* <block-or_exp>`,  has *no effect* until its value is consumed by an `await*`.
Moreover, each additional consumption by an `await*` will trigger a new evaluation of `<block-or-exp>`.

Be careful of this distinction, and other differences, when refactoring code.



### Note:

The `async*` and corresponding `await*` constructs are useful for efficiently abstracting asynchronous code into re-useable functions.
In comparison, calling a local function that returns a proper `async` type requires committing state and suspending execution with each `await` of its result, which can be undesirable.



## Await*

The `await*` expression `await* <exp>` has type `T` provided:

-   `<exp>` has type `async* T`,

-   `T` is shared,

-   the `await*` is explicitly enclosed by an `async`-expression or appears in the body of a `shared` function.
Expression `await <exp>` evaluates `<exp>` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is a delayed computation `<block-or-exp>`. The evaluation of `await* <exp>` proceeds
with the evaluation of `<block-or-exp>`, executing the delayed computation.

### Danger

During the evaluation of `<block-or-exp>`, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes.

### Note

Unlike `await`, which, regardless of the dynamic status of the future, ensures that all tentative state changes and message sends prior to the `await` are committed and irrevocable, `await*` does not, in itself, commit any state changes, nor does it suspend computation.
Instead, evaluation proceeds immediately according to `<block-or-exp>` (the value of `<exp>`), committing state and suspending execution whenever `<block-or-exp>` does (but not otherwise).


### Note

Evaluation of a delayed `async*` block is synchronous while possible, switching to asynchronous when necessary due to a proper `await`.

Using `await*` signals that the computation *may* commit state and suspend execution during the evaluation of `<block-or-exp>`, that is, that evaluation of `<block-or-exp>` may perform zero or more proper `await`s and may be interleaved with the execution of other, concurrent messages.


## TODO:

Future:
- [ ] generics and flattening - rule out generics for now?
- [ ] relax shared content type for `async*` types?

One annoying thing is that we cannot make actor class instantiation yet more efficient without returning  an `async*`, breaking code. Although I guess users could opt in to that if wanted (by giving an `async*` return type). 
That's a drawback compared to the previous `do async/await` approach. But them's the breaks.
  • Loading branch information
@crusso
crusso authored Dec 7, 2022
1 parent cae6684 commit 26c229a
Show file tree
Hide file tree
Showing 95 changed files with 1,203 additions and 349 deletions.
18 changes: 18 additions & 0 deletions Changelog.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,24 @@

* motoko (`moc`)

* Add new keywords `async*` and `await*` (note the `*`) for efficient abstraction of asynchronous code (#3609).
```
<typ> ::= ...
async* <typ> delayed, asynchronous computation
<exp> ::= ...
async* <block-or-exp> delay an asynchronous computation
await* <block-or-exp> execute a delayed computation (only in async, async*)
```
This avoids the resource consumption and latency of `async`/`await` by only committing state and suspending execution
when necessary in the `await*`-ed computation, not necessarily at the `await*` itself.
WARNING: Unlike `async`/`await`:
* an `async*` value has no effect unless `await*`-ed;
* each `await*` of the same `async*` value repeats its effects.
This feature is experimental and may evolve in future. Use with discretion.
See the [manual](doc/md/language-manual.md) for details.
* Suppress GC during IC `canister_heartbeat`, deferring any GC to the scheduled Motoko `heartbeat` `system` method (#3623).
This is a temporary workaround, to be removed once DTS is supported for `canister_heartbeat` itself (#3622).
Expand Down
66 changes: 45 additions & 21 deletions design/asynccps.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ e = x
| if e then e else e
| async e
| await e // may throw
| async* e
| await* e // may throw
| while e do e
| label l e
| break l e
Expand All @@ -30,11 +32,11 @@ e = x

The aim of the game is to remove async and await and try catch/throw by a source-to-source translation, leaving as much code as possible in direct-style.

Terms have effect `T` (trivial) or `A` (await) with `T` < `A`. A term has effect `A` if any subterm not enclosed by `async` is `await`.
Terms have effect `T` (trivial) or `A` (await) with `T` < `A`. A term has effect `A` if any subterm not enclosed by `async` or `async*` is `await` or `await*`.

The only terms that introduce effect `A` is `await`, `try` or `throw` - the effect is masked by its innermost enclosing `async` (if any).
The only terms that introduce effect `A` is `await`, `await*`, `try` or `throw` - the effect is masked by its innermost enclosing `async` or `async*` (if any).

Note `await`, `try` and `throw` may only occur within an `async` block.
Note `await`, `await*`, `try` and `throw` may only occur within an `async` or `async*` block.

The body of every lambda must be trivial.

Expand All @@ -45,9 +47,10 @@ Terms `t` are `await/try/throw` free terms (in the sense that await can only occ
Trivial terms can be compiled in direct style by translation `T[t]`.

Non-trivial terms must be cps-converted by translations `C r [e]` and `CPS[e] r`.
Their translations expect a pair `r = (reply,reject)` and `reply` and `reject` continuations (for interpreting early `return` and `throw`). We write 'r.reply' and `r.reject` for the obvious projections.
The `reply` continuation only changes when we enter an async block.
Their translations expect a pair `r = (reply,reject)` and `reply` and `reject` continuations (for interpreting early `return` and `throw`). We write `r.reply` and `r.reject` for the obvious projections.
The `reply` continuation only changes when we enter an async block.
The `reject` continuation changes when we enter a `async` or `try`.

The translation `C r [e]` produces a term in cps, taking a single continuation argument.

Since `async` and `try catch` are block structured, we can record the
Expand All @@ -71,27 +74,31 @@ C r [ let x = t1 in e2 ] =
C r [ let x = e1 in e2 ] =
\\k.C r [ t1 ] @ (\\x. C r [e2] @ k)
C r [ await t ] =
\\k.await(T[t1], (k, r) )
\\k.await(T[t1], (k, r.reject))
C r [ await e ] =
\\k.C r [e] @ (\\v.await(v,(k,r))
\\k.C r [e] @ (\\v.await(v,(k, r.reject))
C r [ await* t ] =
\\k.T[t1] (k, r.reject)
C r [ await* e ] =
\\k.C r [e] @ (\\v.v (k, r.reject))
C r [ if e1 then e2 else e3 ] =
\\k.C r [e1] @ (\\b.if b then C r [e1]@k else C r [e2]@k)
\\k.C r [e1] @ (\\b.if b then C r [e1] @ k else C r [e2] @ k)
C r [ if t1 then e2 else e3 ] =
\\k.if T[t1] then C r [e1] @ k else C r [e2] @ k
C r [ if e1 then t2 else t3 ] =
\\k.C r [e1] @ (\\b.k @ (if b then T[t1] else T[t2])))
C r [ while t1 do e2 ] =
\\k.
let rec l = \u. if T[t1] then C r [e2]@l else k@u in
let rec l = \u. if T[t1] then C r [e2] @ l else k @ u in
l@()
C r [ while e1 do t2 ] =
\\k.
let rec l = \u. C r [e1](\\v.if v then T[t2] ; l@u else k@u) in
l@()
let rec l = \u. C r [e1](\\v.if v then T[t2] ; l @ u else k @ u) in
l @ ()
C r [ while e1 do e2 ] =
\\k.
let rec l = \u. C r [e1] (\\v.if v then C r [e2]@l else k@()) in
l@()
let rec l = \u. C r [e1] (\\v.if v then C r [e2] @ l else k @ ()) in
l @ ()
C r [ label l e ] = \\l. C r [e] @ l // we use label l to name the success continuation
C r [ break l e ] = \\k. C r [e] @ l // discard k, continue from l
C r [ return e ] = \\k. C r [e] @ r.reply // discard k, exit via r.reply
Expand All @@ -101,11 +108,14 @@ C r [ try e1 with x -> e2 ] =
C r [ throw e] = \\k. C r [e] @ r.reject // discard k, exit async or try via reject
```

The translation of trivial terms, `T[ _ ]`, is homomorphic on all terms but `async _`, at which point we switch to the `CPS[-]` translation.
Note `T[await _]`, `T[throw _]` and `T[try _ with _ -> _]`, are (deliberately) undefined.
In `C`, an `await` is translated by passing the current continuation `k` and reject continuation `r.reject` (both returning answer type `()`) in the promise and yielding if necessary.

The translation of trivial terms, `T[ _ ]`, is homomorphic on all terms but `async _` and `async * _`, at which point we switch to the `CPS[-]` translation.
Note `T[await _]`, `T[throw _]` and `T[try _ with _ -> _]`, are (deliberately) undefined (since they cannot have trivial effect `T`.)

```JS
T[ async e ] = spawn (\t.CPS[e] @ ((\v.complete(t,v)),(\e.reject(t,e)))
T[ async* e ] = CPS[e]
T[ x ]= x
T[ c ] = c
T[ \x.t ] = \x.T[t]
Expand All @@ -121,6 +131,9 @@ T[ label l t ] =
label l T[t]
T[ return T[t] ] =
return T[t]
// if we allow effect(do async e) = effect e (see above), then add case
T[ do async t ] =
CPS*[e] (\v.completedAsync(v), \e.rejectedAsync(e))
```
We use the following primitives for scheduling actions (that complete asyncs).
Expand All @@ -141,12 +154,20 @@ spawn(f) = let t = async { result = Pending; waiters = [] } in
schedule (\u.f(t));
t
await(t,reply,reject) = match t with
| {result = Completed v} -> reply v
| {result = Rejected e} -> reject e
yield() = schedule.Next()
// meta-operations for interpreting `async e`
await(t,(k,r)) = match t with
| {result = Completed v} ->
schedule (\u.k v);
yield();
| {result = Rejected e} -> r e
schedule (\u.r e);
yield();
| {result = Pending} ->
t.waiters <- (k,r)::t.waiters;
yield()
t.waiters <- (k,r)::t.waiters;
yield()
complete(t,v) = match t with
| {result = Pending; waiters} ->
Expand All @@ -162,7 +183,6 @@ reject(t,v) = match t with
schedule(\u.reject(v))
| { result = _ } -> assert(false)
yield() = schedule.Next()
```
The above translations are flawed:
Expand Down Expand Up @@ -203,6 +223,10 @@ T env [ async e ] =
let env' = [l_ret->Cont] in
spawn (\t.CPS env' [e] @ ((\v.complete(t,v)),(\e.reject(t,e)))
T env [ async* e ] =
let env' = [l_ret->Cont] in
CPS env' [e]
T env [\x.t] =
let env' = [l_ret->Label]
\x.T env' [t]
Expand Down
3 changes: 3 additions & 0 deletions doc/md/examples/grammar.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@
<typ_pre> ::=
<typ_un>
'async' <typ_pre>
'async*' <typ_pre>
<obj_sort> <typ_obj>

<typ_nobin> ::=
Expand Down Expand Up @@ -190,7 +191,9 @@
<exp_bin> <binassign> <exp>
'return' <exp>?
'async' <exp_nest>
'async*' <block>
'await' <exp_nest>
'await*' <exp_nest>
'assert' <exp_nest>
'label' <id> (':' <typ>)? <exp_nest>
'break' <id> <exp_nullary>?
Expand Down
92 changes: 87 additions & 5 deletions doc/md/language-manual.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ All comments are treated as whitespace.
The following keywords are reserved and may not be used as identifiers:

``` bnf
actor and assert async await break case catch class continue debug
actor and assert async async* await await* break case catch class continue debug
debug_show do else flexible false for from_candid func if ignore import
in module not null object or label let loop private public query return
shared stable switch system throw to_candid true try type var while with
Expand Down Expand Up @@ -378,7 +378,7 @@ Libraries stored in `.mo` files may be referenced by `import` declarations.

In a module library, the optional name `<id>?` is only significant within the library and does not determine the name of the library when imported. Instead, the imported name of a library is determined by the `import` declaration, giving clients of the library the freedom to choose library names (e.g. to avoid clashes).

An actor class library, because it defines both a type constructor and a function with name `<id>`, is imported as a module defining both a type and a function named `<id>`. The name `<id>` is mandatory and cannot be omitted. An actor class constructor is always asynchronous, with return type `async T` where `T` is the inferred type of the class body. Because actor construction is asynchronous, an instance of an imported actor class can only be created in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function or `async` expression).
An actor class library, because it defines both a type constructor and a function with name `<id>`, is imported as a module defining both a type and a function named `<id>`. The name `<id>` is mandatory and cannot be omitted. An actor class constructor is always asynchronous, with return type `async T` where `T` is the inferred type of the class body. Because actor construction is asynchronous, an instance of an imported actor class can only be created in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function, asynchronous function, `async` expression or `async*` expression).

### Declaration syntax

Expand Down Expand Up @@ -491,6 +491,8 @@ The syntax of an *expression* is as follows:
return <exp>? return
async <block-or-exp> async expression
await <block-or-exp> await future (only in async)
async* <block-or-exp> delay an asynchronous computation
await* <block-or-exp> await a delayed computation (only in async)
throw <exp> raise an error (only in async)
try <block-or-exp> catch <pat> <block-or-exp> catch an error (only in async)
assert <block-or-exp> assertion
Expand Down Expand Up @@ -551,6 +553,7 @@ Type expressions are used to specify the types of arguments, constraints (a.k.a
? <typ> option
<shared>? <typ-params>? <typ> -> <typ> function
async <typ> future
async* <typ> delayed, asynchronous computation
( ((<id> :)? <typ>),* ) tuple
Any top
None bottom
Expand Down Expand Up @@ -776,6 +779,14 @@ The optional `<shared>` qualifier specifies whether the function value is shared

Future types typically appear as the result type of a `shared` function that produces an `await`-able value.

### Async* types

`async* <typ>` specifies a delayed, asynchronous computation producing a value of type `<typ>`.

Computation types typically appear as the result type of a `local` function that produces an `await*`-able value.

(They cannot be used as the return types of `shared` functions.)

### Tuple types

`( ((<id> :)? <typ>),* )` specifies the type of a tuple with zero or more ordered components.
Expand Down Expand Up @@ -1498,7 +1509,7 @@ Note that requirement 1. imposes further constraints on the field types of `T`.

- all public fields must be non-`var` (immutable) `shared` functions (the public interface of an actor can only provide asynchronous messaging via shared functions);

Because actor construction is asynchronous, an actor declaration can only occur in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function or `async` expression).
Because actor construction is asynchronous, an actor declaration can only occur in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function, `async` expression or `async*` expression).

Evaluation of `<sort>? <id>? =? { <dec-field>;* }` proceeds by binding `<id>` (if present), to the eventual value `v`, and evaluating the declarations in `<dec>;*`. If the evaluation of `<dec>;*` traps, so does the object declaration. Otherwise, `<dec>;*` produces a set of bindings for identifiers in `Id`. let `v0`, …​, `vn` be the values or locations bound to identifiers `<id0>`, …​, `<idn>`. The result of the object declaration is the object `v == sort { <id0> = v1, …​, <idn> = vn}`.

Expand Down Expand Up @@ -2152,7 +2163,7 @@ The expression `return <exp>` has type `None` provided:

- `async T` is the type of the nearest enclosing (perhaps implicit) `async` expression (with no intervening function declaration)

The `return` expression exits the corresponding dynamic function invocation or completes the corresponding dynamic async expression with the result of `<exp>`.
The `return` expression exits the corresponding dynamic function invocation or completes the corresponding dynamic `async` or `async*` expression with the result of `<exp>`.

### Async

Expand Down Expand Up @@ -2186,6 +2197,77 @@ Note: suspending computation on `await`, regardless of the dynamic status of the

Between suspension and resumption of a computation, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes.

Using `await` signals that the computation *will* commit its current state and suspend execution.

:::

### Async*

The async expression `async* <block-or-exp>` has type `async* T` provided:

- `<block-or-exp>` has type `T`;

- `T` is shared.

Any control-flow label in scope for `async* <block-or-exp>` is not in scope for `<block-or-exp>`. However, `<block-or-exp>` may declare and use its own, local, labels.

The implicit return type in `<block-or-exp>` is `T`. That is, the return expression, `<exp0>`, (implicit or explicit) to any enclosed `return <exp0>?` expression, must have type `T`.

Evaluation of `async* <block-or-exp>` produces a delayed computation to evaluate `<block-or-exp>`. It immediately returns a value of type `async* T`.
The delayed computation can be executed using `await*`, producing one evaluation
of the computation `<block-or-exp>`.

:::danger

Note that `async <block-or-exp>` has the effect of scheduling a single asynchronous computation of `<exp>`, regardless of whether its result, a future, is consumed with an `await`.
Moreover, each additional consumption by an `await` just returns the previous result, without repeating the computation.

In comparison, `async* <block-or_exp>`, has *no effect* until its value is consumed by an `await*`.
Moreover, each additional consumption by an `await*` will trigger a new evaluation of `<block-or-exp>`, including repeated effects.

Be careful of this distinction, and other differences, when refactoring code.

:::

:::note

The `async*` and corresponding `await*` constructs are useful for efficiently abstracting asynchronous code into re-useable functions.
In comparison, calling a local function that returns a proper `async` type requires committing state and suspending execution with each `await` of its result, which can be undesirable.

:::


### Await*

The `await*` expression `await* <exp>` has type `T` provided:

- `<exp>` has type `async* T`,

- `T` is shared,

- the `await*` is explicitly enclosed by an `async`-expression or appears in the body of a `shared` function.
Expression `await <exp>` evaluates `<exp>` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is a delayed computation `<block-or-exp>`. The evaluation of `await* <exp>` proceeds
with the evaluation of `<block-or-exp>`, executing the delayed computation.

:::danger

During the evaluation of `<block-or-exp>`, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes.

:::

:::note

Unlike `await`, which, regardless of the dynamic status of the future, ensures that all tentative state changes and message sends prior to the `await` are committed and irrevocable, `await*` does not, in itself, commit any state changes, nor does it suspend computation.
Instead, evaluation proceeds immediately according to `<block-or-exp>` (the value of `<exp>`), committing state and suspending execution whenever `<block-or-exp>` does (but not otherwise).

:::

:::note

Evaluation of a delayed `async*` block is synchronous while possible, switching to asynchronous when necessary due to a proper `await`.

Using `await*` signals that the computation *may* commit state and suspend execution during the evaluation of `<block-or-exp>`, that is, that evaluation of `<block-or-exp>` may perform zero or more proper `await`s and may be interleaved with the execution of other, concurrent messages.

:::

### Throw
Expand All @@ -2196,7 +2278,7 @@ The `throw` expression `throw <exp>` has type `None` provided:

- the `throw` is explicitly enclosed by an `async`-expression or appears in the body of a `shared` function.

Expression `throw <exp>` evaluates `<exp>` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is an error value `e`. Execution proceeds from the `catch` clause of the nearest enclosing `try <block-or-exp1> catch <pat> <block-or-exp2>` whose pattern `<pat>` matches value `e`. If there is no such `try` expression, `e` is stored as the erroneous result of the `async` value of the nearest enclosing `async` expression or `shared` function invocation.
Expression `throw <exp>` evaluates `<exp>` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is an error value `e`. Execution proceeds from the `catch` clause of the nearest enclosing `try <block-or-exp1> catch <pat> <block-or-exp2>` whose pattern `<pat>` matches value `e`. If there is no such `try` expression, `e` is stored as the erroneous result of the `async` value of the nearest enclosing `async`, `async*` expression or `shared` function invocation.

### Try

Expand Down
8 changes: 7 additions & 1 deletion emacs/motoko-mode.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,21 +34,26 @@
'("actor"
"and"
"async"
"async*"
"assert"
"await"
"await*"
"break"
"case"
"catch"
"class"
"continue"
"do"
"debug"
"debug_show"
"else"
"flexible"
"for"
"from_candid"
"func"
"if"
"in"
"ignore"
"import"
"module"
"not"
Expand All @@ -59,15 +64,16 @@
"loop"
"private"
"public"
"query"
"return"
"shared"
"stable"
"switch"
"system"
"try"
"throw"
"to_candid"
"with"
"query"
"type"
"var"
"while"
Expand Down
Loading

0 comments on commit 26c229a

Please sign in to comment.