25 Actors — living with state, by messages

25.1 Declare, make, talk#

module counter_demo .
rem run: use_counter

actor counter do
  state do
    value u64 .
  end

  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end

  fn get output u64 .
  do
    return value .
  end
end

proc use_counter output u64 . effects state .
do
  var c counter be spawn actor counter .
  let a u64 be send c inc .
  let b u64 be send c inc .
  return send c get .
end

$ lowentc --run use_counter counter.low
use_counter() = 2

• actor counter do … end declares an actor. state do value u64 . end is its state, which exists only inside the actor and cannot be touched directly from outside.
• inc, which changes the state, is a proc with effects state. get, which only reads, is a fn. Ops inside actors follow the kind rules of chapter 5 as is.
• var c counter be spawn actor counter . makes one actor. Its state starts at 0.
• send c inc sends the inc message to c, waits until it is handled, and receives the result.

An actor handles messages one at a time. So its state is never touched concurrently. That is why there is no need to take locks by hand.

Think of a bank with a single counter. Customers (messages) queue, and the clerk (the actor) serves one customer at a time. The vault (the state) is behind the counter, so no customer can open it directly.

  senders                        mailbox (queue)          actor counter
                                                     ┌──────────────────────┐
  send c inc  ───────▶ ┌─────┬─────┬─────┐           │  handling now: inc   │
  send c inc  ───────▶ │ inc │ inc │ get │ ────────▶ │                      │
  send c get  ───────▶ └─────┴─────┴─────┘ one by one│  state: value = 1    │ ← not reachable from outside
                                                     └──────────────────────┘

Because messages leave the queue one at a time, two messages never change value at the same moment.

Writing fn for something that changes state is rejected.

module pure_bad .
rem expect: E-EFFECT-PURITY

actor counter do
  state do
    value u64 .
  end

  fn inc output u64 .
  do
    set value (add value 1) .
    return value .
  end
end

$ lowentc --check pure_bad.low
pure_bad.low:9:0 E-EFFECT-PURITY: a `fn` message handler WRITES the actor's STATE — and that write is visible to the NEXT message. A fn is an enforced purity contract (SPEC-003 §27): callers may memoise, reorder or elide it. Declare it a `proc` (and say `effects state`). ★ Nobody used to look here: handlers were declared with `on`, which said NOTHING about pure-vs-procedural, and the IR read that as PURE. RFC-0046 removed the bare-`op` default exactly so the 1 bit is always stated — `on` had put it back. RFC-0057
pure_bad.low:10:3 E-EFFECT-CALC: this fn is declared pure but performs `state` — make it a `proc` with `effects …`, or remove the effect

As the diagnostic says, that write is visible to the next message. If a caller remembered results or reordered calls, the answer would be wrong.

25.2 Carrying values in messages#

Values are written side by side after the message name. On the receiving side the actor itself is treated like the first parameter, and the carried values follow.

module args .
rem run: tally 5 7

actor account do
  state do
    balance u64 .
  end

  proc deposit input amount u64 . output u64 . effects state .
    requires le amount 1000000 .
  do
    set balance (wrap_add balance amount) .
    return balance .
  end
end

proc tally input a u64 . input b u64 . output u64 . effects state .
  requires le a 1000000 .
  requires le b 1000000 .
do
  var acct account be spawn actor account .
  let x u64 be send acct deposit a .
  return send acct deposit b .
end

$ lowentc --run tally args.low 5 7
tally(5, 7) = 12

send acct deposit a puts a into deposit’s amount. Message ops can have contracts too.

Sending a value with ownership hands the ownership over.

module handoff .
rem expect: E-OWN-MOVED

type job u64 .

actor worker do
  state do
    done u64 .
  end
  proc take input j owned job . output u64 . effects state .
  do
    drop j .
    set done (add done 1) .
    return done .
  end
end

proc give_twice input n u64 . output u64 . effects state .
do
  var w worker be spawn actor worker .
  var j owned job be n .
  let a u64 be send w take j .
  return send w take j .
end

$ lowentc --check handoff.low
handoff.low:23:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

Once j has gone out with the first message, give_twice can no longer use j. When two flows hold the same value together, races arise. When ownership travels only by message, only one party can touch the value at any moment, and a race is not so much prevented as left no place to happen.

25.3 Mailboxes — putting in and emptying#

send waits until handling finishes. Deliveries whose results are not needed are only put into the mailbox with spawn send.

module mailbox .
rem run: drive
rem run: nodrain

actor counter do
  state do
    v u64 .
  end
  proc inc output u64 . effects state .
  do
    set v (add v 1) .
    return v .
  end
  fn get output u64 .
  do
    return v .
  end
end

proc drive output u64 . effects state .
do
  var c counter be spawn actor counter .
  spawn send c inc .
  spawn send c inc .
  spawn send c inc .
  drain c .
  return send c get .
end

proc nodrain output u64 . effects state .
do
  var c counter be spawn actor counter .
  spawn send c inc .
  spawn send c inc .
  return send c get .
end

$ lowentc --run drive mailbox.low
drive() = 3
$ lowentc --run nodrain mailbox.low
nodrain() = 0

drive puts inc in three times, empties the mailbox in the order put in with drain c, and then reads 3. nodrain did not empty it, so the result is 0. Messages in a mailbox are not handled by themselves.

The processor does not decide delivery times on its own for the sake of determinism. The same program must give the same answer, and the delivery time is the answer. Because a person picks where to empty, the VM and native code deliver in the same order, and the cross-check of two back ends keeps it so. schedule . empties the mailboxes of every actor at once. Fixing the mailbox size with mailbox bounded 2 . makes overflowing puts stop, and try spawn send gives the error as a value instead of stopping.

25.4 Let it crash, then restart#

When an actor’s op panics, the actor can be restarted. Its state returns to the beginning and the message is handled again.

module restart .
rem run: recover
rem trap: escalate

actor recov do
  state do
    bad u64 .
  end
  failure restart max 3 .
  proc step output u64 . effects state panic .
  do
    if ne bad 0 . do
      panic "corrupted state" .
    end
    set bad 1 .
    return 42 .
  end
end

actor doomed do
  state do
    v u64 .
  end
  failure restart max 2 .
  proc boom output u64 . effects state panic .
  do
    panic "always fails" .
    return 0 .
  end
end

proc recover output u64 . effects state panic .
do
  var c recov be spawn actor recov .
  let x u64 be send c step .
  return send c step .
end

proc escalate output u64 . effects state panic .
do
  var c doomed be spawn actor doomed .
  return send c boom .
end

$ lowentc --run recover restart.low
recover() = 42
$ lowentc --run escalate restart.low
== ir diagnostics (1) ==
0:0 E-VM-PANIC: the program called `panic` — this is an unrecoverable stop, and it is NOT a contract violation (the code chose to stop, it did not break a promise)

• recov sets bad to 1 on the first step and panics on the second. With failure restart max 3 ., the state goes back to the start (bad = 0) and the message is handled again, giving 42.
• doomed always crashes. If it still crashes after two restarts, the failure goes upwards and the program stops. No actor is left silently stopped.

There are three policies — restart max <count> (that many times), never (pass upwards on the first crash) and always (restart without counting). Restarting applies only to panic. A contract violation is the program breaking a promise it wrote itself, and doing it again gives the same result, so it is not restarted. Only the actor’s own state is revived; other actors are not touched.

Code that undoes, one by one, failures where state became strange by chance is long, and long code is itself wrong. Resetting the state to the beginning is a short recovery that is always right.

25.5 Where actors may be used#

A program can state where it runs with build profile <name> .. When it does, concurrency that place cannot support is rejected at translation.

module profile .
rem expect: E-PROFILE-LEVEL

build profile embedded .

actor counter do
  state do
    value u64 .
  end
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
end

$ lowentc --check profile.low
4:0 E-PROFILE-LEVEL: this module uses a CONCURRENCY FEATURE its build profile does not provide (RFC-0009 §105/§139): freestanding has no concurrency at all, embedded has a static task graph, native adds jobs/green threads, server adds actors. The level is not declared — it is COMPUTED from the constructs you used — and the profile caps it. Either raise the profile or stop using the feature

Declaring an actor alone is level 3. Without a profile, nothing is restricted — only whoever writes it takes on the promise.

25.6 Actors that hold a capability, and what state may contain#

An actor’s state may have a capability field. A capability is a mark that exists only at translation, so the field has no size at run time. In return, a rule fixes what fills it.

module capfield .
rem run: main

rem a log book that carves 16 bytes from the fixed window for each entry
actor logbook do
  state do
    rem a capability field; it has no size at run time and is filled from the capability at the spawn site
    root cap allocator .
    entries u64 .
  end
  proc write input code u8 . output bool . effects alloc state . do
    let g option mut slice u8 . . be alloc_bytes root capacity 16 .
    guard is_some g . else return false .
    let v mut slice u8 . . be some_value g .
    set (index v 0) code .
    set entries (add entries 1) .
    return true .
  end
  fn count output u64 . do
    return entries .
  end
end

proc main input al cap allocator . output u8 . effects alloc state .
do
  var book logbook be spawn actor logbook .
  let a bool be send book write 7 .
  let b bool be send book write 9 .
  return narrow u8 (send book count) .
end

$ lowentc --run main capfield.low
main() = 2

• root cap allocator . is the capability field. write calls alloc_bytes root capacity 16 through it, so the capability need not be passed as an argument in every message.
• spawn actor logbook is allowed because main received cap allocator. The field is filled with the capability at the spawn site.
• After two entries, count answers 2.

An op that did not receive the capability is refused when it spawns the same actor.

module mistake_capfield .
rem expect: E-CAP-FORGE

actor logbook do
  state do
    root cap allocator .
    entries u64 .
  end
  proc write input code u8 . output bool . effects alloc state . do
    let g option mut slice u8 . . be alloc_bytes root capacity 16 .
    guard is_some g . else return false .
    set entries (add entries 1) .
    return true .
  end
end

rem ✘ an op that was not handed cap allocator spawns an actor with a capability field
proc sneaky output u64 . effects alloc state .
do
  var book logbook be spawn actor logbook .
  let a bool be send book write 7 .
  return 0 .
end

$ lowentc --check mistake_capfield.low
mistake_capfield.low:20:0 E-CAP-FORGE: this spawns an actor whose state HOLDS a capability (`cap allocator` / `cap heap`), but the op spawning it holds no capability of that kind. A capability field means nothing at run time — it is only real because the place that creates the actor already had the right. Without that, one `spawn` would forge authority out of thin air (RFC-0112 D6). Take the capability as an input of this op

If this were allowed, one spawn line would conjure a capability out of nothing. A capability field only records the fact that “the place that created this actor already held the capability”. The standard allocators allocs.fixed_bytes and heap_bytes are ordinary actors that follow this rule (chapter 20).

This is what a state field may and may not hold.

25.7 Designing with actors — a transfer between two accounts#

This section gathers the pieces so far into one design. Each account is an actor, and a transfer is an op that talks to the two actors in turn.

module transfer .
rem run: move 30
rem run: move 80

enum bank_error do
  insufficient .
end

actor account do
  state do
    balance u64 .
  end

  rem add to the balance --- it changes state, so it is a proc
  proc deposit input amount u64 . output u64 . effects state .
    requires le amount 1000000 .
  do
    set balance (wrap_add balance amount) .
    return balance .
  end

  rem if short, leave the state untouched and return the error as a value
  proc withdraw input amount u64 . output result u64 bank_error . effects state .
    errors insufficient .
  do
    guard le amount balance . else return error insufficient .
    set balance (sub balance amount) .
    return ok balance .
  end

  fn peek_balance output u64 .
  do
    return balance .
  end
end

rem a transfer between two actors --- deposit only when the withdrawal succeeded
proc move input amount u64 . output u64 . effects state .
  requires le amount 1000 .
do
  var src account be spawn actor account .
  var dst account be spawn actor account .
  let seed u64 be send src deposit 50 .
  let r result u64 bank_error be send src withdraw amount .
  guard not (is_error r) . else return add (mul (send src peek_balance) 1000) (send dst peek_balance) .
  let t u64 be send dst deposit amount .
  return add (mul (send src peek_balance) 1000) (send dst peek_balance) .
end

$ lowentc --run move transfer.low 30
move(30) = 20030
$ lowentc --run move transfer.low 80
move(80) = 50000

• The balance lives only in the state of account. The outside reaches an account only through three messages: deposit, withdraw and peek_balance.
• When the balance is short, withdraw returns error insufficient without touching the state. It does not stop — a short balance is a failure the account’s user can handle (chapter 17).
• move deposits only when the withdrawal succeeded. move 30 leaves 20 with the sender and 30 with the receiver, giving 20030. With move 80 the withdrawal fails and both accounts stay at 50 and 0 (50000).
• Messages are processed one at a time, so no other message can slip in between withdraw checking the balance and reducing it. The race between “check, then write” does not exist in this shape.

The errors insufficient . of withdraw has no condition on purpose. The fourth item of “Common mistakes” below explains why.

25.8 Common mistakes#

module mistake_bounded .
rem trap: burst

actor counter do
  state do
    value u64 .
  end
  mailbox bounded 2 .
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
  fn get output u64 .
  do
    return value .
  end
end

proc burst output u64 . effects state .
do
  var c counter be spawn actor counter .
  spawn send c inc .
  spawn send c inc .
  rem ✘ the mailbox holds two, yet a third is put in before draining
  spawn send c inc .
  drain c .
  return send c get .
end

$ lowentc --run burst mistake_bounded.low
== ir diagnostics (1) ==
0:0 E-VM-MAILBOX-FULL: the actor's bounded mailbox is full — `spawn send` would exceed `mailbox bounded N` pending messages (drain it first, or raise N)

module bounded_fixed .
rem run: burst

actor counter do
  state do
    value u64 .
  end
  mailbox bounded 2 .
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
  fn get output u64 .
  do
    return value .
  end
end

proc burst output u64 . effects state .
do
  var c counter be spawn actor counter .
  spawn send c inc .
  spawn send c inc .
  rem if it cannot be put in, receive the error as a value instead of stopping --- drain, then put it in again
  let r result u64 mailbox_full be try spawn send c inc .
  if is_error r . do
    drain c .
    spawn send c inc .
  end
  drain c .
  return send c get .
end

$ lowentc --run burst bounded_fixed.low
burst() = 3

module mistake_unknownmsg .
rem expect: E-IR-UNDEF

actor counter do
  state do
    value u64 .
  end
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
end

proc use_counter output u64 . effects state .
do
  var c counter be spawn actor counter .
  rem ✘ `counter` does not handle a `dec` message
  return send c dec .
end

$ lowentc --check mistake_unknownmsg.low
mistake_unknownmsg.low:19:0 E-IR-UNDEF: send names a message this actor does not handle (the handler is looked up IN THE RECEIVER'S TYPE — it used to be found by BARE NAME, so two actors with a handler of the same name silently shared one)

module mistake_peekstate .
rem expect: E-ACTOR-FIELD

actor counter do
  state do
    value u64 .
  end
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
end

proc peek output u64 . effects state .
do
  var c counter be spawn actor counter .
  let a u64 be send c inc .
  rem ✘ reads the actor's state field from outside --- this should be blocked, but passes in this edition
  return field c value .
end

$ lowentc --check mistake_peekstate.low
mistake_peekstate.low:20:0 E-ACTOR-FIELD: this reads a STATE FIELD of an actor from outside it. An actor's state lives inside the actor and nowhere else (§10.2): the only door is a message (`send a <op> …`). If the state were readable from outside, the isolation that makes actors safe without locks — one message at a time — would not hold, and the reader would see a value between two messages. Add an op to the actor that returns what you need

module mistake_errorsstate .
rem expect: E-ERRORS-STATE

enum bank_error do
  insufficient .
end

actor account do
  state do
    balance u64 .
  end

  proc deposit input amount u64 . output u64 . effects state .
    requires le amount 1000000 .
  do
    set balance (wrap_add balance amount) .
    return balance .
  end

  rem ✘ the error condition reads the state field `balance` --- on exit it is read again, after the balance has shrunk
  proc withdraw input amount u64 . output result u64 bank_error . effects state .
    errors insufficient gt amount balance .
  do
    guard le amount balance . else return error insufficient .
    set balance (sub balance amount) .
    return ok balance .
  end
end

proc take30 output u64 . effects state .
do
  var a account be spawn actor account .
  let seed u64 be send a deposit 50 .
  let r result u64 bank_error be send a withdraw 30 .
  guard not (is_error r) . else return 1 .
  return ok_value r .
end

var fee u64 be 5 .

rem ✘ the same holds outside an actor --- a module `var` and a `mut` argument can both be changed by the body, so neither may stand in an error condition
proc charge input amount u64 . input log mut slice u8 . . output result u64 bank_error . effects state .
  errors insufficient lt amount fee .
do
  set fee 0 .
  return ok amount .
end

$ lowentc --check mistake_errorsstate.low
mistake_errorsstate.low:42:0 E-ERRORS-STATE: the condition of this `errors` clause names something whose value can DIFFER between entry and exit — an actor state field, a module `var`, or a `mut` parameter. An `errors` condition is read on the values the op was ENTERED with (canon §6.4.2): the clause says what the CALLER got wrong, and what the caller handed over is all it can be blamed for. A name the body may change cannot carry that meaning — read on exit it accuses the op of owing an error it never owed. Write the condition over the inputs that do not change (and module constants), and guard on the changing thing inside the body
21:0 E-ERRORS-STATE: the condition of this `errors` clause names something whose value can DIFFER between entry and exit — an actor state field, a module `var`, or a `mut` parameter. An `errors` condition is read on the values the op was ENTERED with (canon §6.4.2): the clause says what the CALLER got wrong, and what the caller handed over is all it can be blamed for. A name the body may change cannot carry that meaning — read on exit it accuses the op of owing an error it never owed. Write the condition over the inputs that do not change (and module constants), and guard on the changing thing inside the body
mistake_errorsstate.low:42:0 E-NAME-BUILTIN: a PARAMETER takes the name of a builtin op — inside this op the name now means two things, and which one it means decides how the sentence is bracketed (RFC-0046 P1). Rename the parameter

module mistake_reffield .
rem expect: E-ACTOR-STATE-REF

actor holder do
  state do
    rem ✘ keeping a borrow in state; there is no place that says what it borrows
    r ref u64 .
  end
  fn peek output u64 . do
    return deref r .
  end
end

proc peek_it output u64 . effects state .
do
  var h holder be spawn actor holder .
  return send h peek .
end

$ lowentc --check mistake_reffield.low
7:0 E-ACTOR-STATE-REF: an actor STATE field may not be a borrow (`ref` / `mut_ref`). A borrow may not outlive what it borrows (§8.4.1), and a state field lives as long as the actor — there is nowhere here to say what it borrows. Keep a VALUE in state (copy it in), or keep a slice the actor was handed and owns for its lifetime
mistake_reffield.low:17:0 E-ACTOR-UNINIT: this is the FIRST message sent to an actor that was just spawned, and the handler READS a state field that holds a slice without setting it. A fresh actor's state is all zeroes, and zero is not a slice: the VM stops (`len needs a slice`) while native quietly answers `none` — the two back ends disagree, which means one of them is lying. Send the message that sets it up first (the one whose handler `set`s that field, typically `init`)

module restart_resets .
rem run: three_incs

actor counter do
  state do
    value u64 .
  end
  failure restart max 3 .
  proc inc output u64 . effects state panic .
  do
    rem blows up once, when the value is 2
    if eq value 2 . do panic "at two" . end
    set value (add value 1) .
    return value .
  end
end

proc three_incs output u64 . effects state panic .
do
  var c counter be spawn actor counter .
  let a u64 be send c inc .
  let b u64 be send c inc .
  rem the third message blows up, the state goes back to 0, and this message is processed again
  return send c inc .
end

$ lowentc --run three_incs restart_resets.low
three_incs() = 1

module separate_state .
rem run: two_counters

actor counter do
  state do
    value u64 .
  end
  proc inc output u64 . effects state .
  do
    set value (add value 1) .
    return value .
  end
end

proc two_counters output u64 . effects state .
do
  var left counter be spawn actor counter .
  var right counter be spawn actor counter .
  let a u64 be send left inc .
  let b u64 be send left inc .
  rem `right` has its own state --- the result is 1
  return send right inc .
end

$ lowentc --run two_counters separate_state.low
two_counters() = 1

25.9 This chapter’s syntax at a glance#