Consider adding an *atomic* expression (syntax `atomic <exp>`)

[crusso]

The idea is that this would prevent sending/awaiting from within exp (and the concurrency issues this raises due to interleavings) and would be useful for enforcing atomic sections of async method bodies.

It should be easy to enforce using the existing type systems (and could indeed just be coded as a higher-order function at the moment).

[robin-kunzler]

The motivation for this from a security perspective are issues relating to inter-canister calls and rollbacks. See also the security best practices here. We found ‘time-of-check time-of-use’ issues several times, e.g. where a condition is checked, and then a call to a canister (e.g. a transfer) is issued. This can lead to situations where transfers are made without the conditions being true.

If certain critical sections (e.g. check a condition and then modify the state) could be marked atomic, the hope is that this could help to make it harder to introduce this kind of bugs later.

[ggreif]

I don’t think the atomic keyword conveys the right semantics. If we can break or return out of it then it is not atomic in the “indivisible” meaning of the word. What we should convey is that it won’t relinquish control (non-await), so maybe instant would be the right term. Or maybe synchronous.

[nomeata]

Related: https://github.com/dfinity/motoko/issues/792

[crusso]

Yeah atomic might be too reminiscent of STM/transactions. critical { } might work.

Though if you compiled the atomic to an await-free async, then it would have the all or nothing transactional flavour (but itself introduce an undesired context switch).

[crusso]

How about relentlessly { ... }? ;->

[matthewhammer]

How about relentlessly { ... }? ;->

In all seriousness, using some word that references the keyword await somehow, in a negative way, would be ideal (and not repurposing the word atomic, for all of the reasons mentioned by @rossberg on Slack and @nomeata and @crusso above).

How about sync { }, meaning, "no asynchronous await control flow."

Update: Oh, looks like I'm +1 to this suggestion, first above by @nomeata

[crusso]

Screen scrape of slack discussion https://dfinity.slack.com/archives/CPL67E7MX/p1651743314819839

Folks, @Jens Groth @Robin Künzler are interested in us adding atomic blocks for use in async contexts, to delineate bits of code that must run atomically and cannot await (and possibly cannot queue up sends - not sure about that). E.g.

shared func transfer(src: Nat, dst : Nat, amount : Nat) : async () {
    atomic {
         accounts[src] -= amount;
         // await havoc(); verboten
         accounts[dst] += amount;
    }
}

I think it's fairly trivial to implement - just adjusting the capability field in the context. Thoughts? (edited)

The idea is that this would prevent sending/awaiting from within exp (and the concurrency issues this raises due to interleavings) and would be useful for enforcing atomic sections of async method bodies. It should be easy to enforce using the existing type systems (and could indeed just be coded as a higher-order function at the moment).

14 replies

Gabor Greif [5 days ago]

Maybe we should think of a (in-the-future) syntax that also can add invariants and pre/postconditions to such a block. These would get compiled away, unless the --debug flag is supplied to moc.

Gabor Greif 5 days ago This feature basically means that (in CPS terms) the continuation is not in scope inside of the atomic block?

Claudio Russo 5 days ago I think the cps conversion remains unchanged, though the body could probably always be compiled in direct style in our selective cps conversion. It just means that you cannot pass the continuations to an await expression. You could still return or throw from the block, invoking the enclosing continuations. It just means there is no possibility of inter-leavings occurring within the block. (edited)

Gabor Greif 5 days ago Right, the block not having access to the success continuation would imply that it has to be compiled in direct style. (This is just for the sake of my mental model.)

Claudio Russo 5 days ago No the success continuation would still be be available so you could return from the atomic block, unless we want to rule that out too. The failure continuation may indeed not be - I'd have to look how closely that was tied to the await capability. It was all a bit adhoc. :heavy_check_mark: 1

Claudio Russo 5 days ago Maybe we should think of a (in-the-future) syntax that also can add invariants and pre/postconditions to such a block. These would get compiled away, unless the --debug flag is supplied to moc. Not sure about that - I think you'd want pre/post on functions, perhaps a global invariant to verify at every await and maybe regular invariants on loops. Probably best to move further discussion to the PR though.

Andreas Rossberg 5 days ago

I'm not convinced at all. First of all, this adds no expressiveness to the language, technically, it's merely documentation. Second, what I think this will actually add is a massive amount of confusion among developers, who will now assume that normal execution is not actually atomic. Explicit atomic sections are also is totally contrary in spirit to the actor model, one of whose major points it is to make atomic the default (async notwithstanding). What's the motivation for this, if I may ask?

Claudio Russo 5 days ago It's a little more than documentation since it prevents the user from awaiting in its body - but yes, I believe @Robin Künzler and @Jens Groth just want it to be able to highlight and protect sections that should not be made non-atomic by accidental insertion of an await. It's only desirable because we deviated from the actor model by allowing messages to suspend opening the door to non-atomicity. (edited) :+1: 1

Claudio Russo 5 days ago FWIW, you actually had it on the roadmap, unless I smuggled it in undetected. I don't feel strongly about this. (edited)

2303

Robin Künzler: 5 days ago @Andreas Rossberg Thanks for joining the discussion. The motivation for this discussion were security issues we found relating to inter-canister calls and rollbacks. See also the security best practices here. We found ‘time-of-check time-of-use’ issues several times, e.g. where a condition is checked, and then a call to a canister (e.g. a transfer) is issued. This can lead to situations where transfers are made without the conditions being true. If certain critical sections (e.g. check a condition and then modify the state) could be marked atomic, the hope is that this could help to make it harder to introduce this kind of bugs later.

Gabor Greif [5 days ago]

I don’t think the atomic keyword conveys the right semantics. If we can break or return out of it then it is not atomic in the “indivisible” meaning of the word. What we should convey is that it won’t relinquish control (non-await), so maybe instant would be the right term.

https://github.com/dfinity/motoko|dfinity/motokodfinity/motoko | May 5th | Added by GitHub

Matthew Hammer 4 days ago

It’s only desirable because we deviated from the actor model by allowing messages to suspend opening the door to non-atomicity.

Yes, and it’s additionally interesting to me that sync { } (if we add it, and call it that) is about explicitly documenting and enforcing the absence of that, and the denial certain code evolutions, and has no other meaning at all. I wonder about other useful variations, like trapless. But then we’d start to need a general effect system.

Andreas Rossberg 3 days ago

It's a little more than documentation since it prevents the user from awaiting in its body Yes, but then you don't have a legal program. If the program is actually legal, atomic does nothing, you can just as well remove it, which makes it rather misleading, since that's not how atomic blocks work elsewhere. We found ‘time-of-check time-of-use’ issues several times Right, but atomic blocks don't really address that, they merely provide a false sense of security in trivial cases. The language team has repeatedly discussed that we need type system checks against unintended state/data dependencies across awaits (a.k.a. yield points). That's much more useful, since of course you often actually need an async call – and that's where you need checks from the compiler most! A blunt "atomic" block makes compiler checks mutually exclusive with calls, which is rather unhelpful. Unfortunately, that is harder to design. But I think much more worthwhile.

Claudio Russo 16 hours ago

Yes, but then you don't have a legal program. If the program is actually legal, atomic does nothing, you can just as well remove it, which makes it rather misleading, since that's not how atomic blocks work elsewhere.

I don't disagree, but similar arguments could be applied to type abstraction - removing a type abstraction doesn't affect the behaviour of the code, but does allow more violations of invariants by subsequent refactoring. I guess the question we could ask is if there is any evidence (i.e. examples of code evolution) that implicitly atomic blocks were broken by later commits that inserted awaits? Or was (as I suspect) the code broken from the beginning anyway? (edited)

[crusso]

Given the amount of pushback, perhaps we could just offer the library based solution:

Messaging.mo:
atomically : (func () -> ()) -> ();

And

import {atomically} = "mo:base/Messaging";
...
shared func transfer(src: Nat, dst : Nat, amount : Nat) : async () {
   atomically (func () {
         accounts[src] -= amount;
         // await havoc(); verboten
         accounts[dst] += amount;
   });
}

This prevents any sends or await from the lambda body, without further ado, but also rules out jumps to enclosing labels and other imperative control flow (including return from enclosing function) which may or may not be seen as a bonus.

Bit more expensive though, given our current compiler....

[rossberg]

@crusso:

similar arguments could be applied to type abstraction

Not quite, type abstraction restricts contexts, i.e., client code. The atomic block as discussed here has no such effect, it's merely a fancy static assertion. (Calling it assert atomic {} would perhaps be more to the point. :) )