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 spawn actor counter . .
  let a u64 send c. inc . .
  let b u64 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 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 spawn actor account . .
  let x u64 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 spawn actor worker . .
  var j owned job n. .
  let a u64 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 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 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. There too the messages to one actor are handled one at a time in the order put in, and even if a handler yields, the next message goes only after the earlier one has finished. The order between different actors is not fixed, so a program that leans on it is caught by a schedule explore_interleavings test. Draining an actor while it is still handling a message from its mailbox stops the program (E-VM-DRAIN-BUSY) — drain it after that message has finished. 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 tick 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 spawn actor recov . .
  let x u64 send c. tick . .
  return send c. tick . .
end .

proc escalate output u64 . effects state panic .
do
  var c doomed 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 tick 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, all written after failure 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. The same holds for a message sent with spawn send and delivered by drain or schedule. The messages still waiting in that actor’s mailbox are not thrown away — the restarted actor handles them in the order they were put in (spawn send has already returned saying it took them).

A period can be attached, as in restart max 3 within 1 minute. The units are second, minute and hour, written seconds and so on for more than one. This edition’s processor only records the period, though. It keeps the count (max) but does not yet count “within one minute”, and says so with the warning W-NOT-YET. If a design leans on time for its recovery, read that warning and check that the count alone is safe.

An actor has one failure policy. The same holds for the mailbox policy (mailbox).

module mistake_twopolicies .
rem expect: E-ACTOR-FAILURE

actor worker do
  state do
    n u64 .
  end .
  rem ✘ two failure policies
  failure restart max 3 .
  failure restart never .
  proc tick output u64 . effects state .
  do
    set n. add n. 1 . .
    return n. .
  end .
end .

$ lowentc --check mistake_twopolicies.low
10:0 E-ACTOR-FAILURE: an actor declares `failure` twice — one restart policy per actor

With two policies the text does not say which one stands, and the answer becomes the processor’s private business. So it is refused with E-ACTOR-FAILURE (two mailbox policies are E-ACTOR-MAILBOX).

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 alloc_bytes root. capacity 16 . .
    guard is_some g. . else return false . .
    let v mut slice u8 some_value g. . .
    set idx 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 spawn actor logbook . .
  let a bool send book. write 7 . .
  let b bool 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 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 spawn actor logbook . .
  let a bool 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 spawn actor account . .
  var dst account spawn actor account . .
  let seed u64 send src. deposit 50 . .
  let r result u64 bank_error 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 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 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 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 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 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 spawn actor counter . .
  let a u64 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 spawn actor account . .
  let seed u64 send a. deposit 50 . .
  let r result u64 bank_error send a. withdraw 30 . .
  guard not is_error r. . . else return 1 . .
  return ok_value r. . .
end .

var fee u64 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:43:0 W-ERRORS-UNRAISED: this `errors` clause names a failure the body never returns. The clause is read as a promise about what this op can do, and the callers write their handling from it — a branch that can never be taken is dead code the reader cannot tell from live code. Return it (`return error <variant>`), forward one (`try`), or remove the clause

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 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 spawn actor counter . .
  let a u64 send c. inc . .
  let b u64 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 spawn actor counter . .
  var right counter spawn actor counter . .
  let a u64 send left. inc . .
  let b u64 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#