module arch.node.engines.executor;

import prelude open;
import arch.node.types.engine open;
import arch.node.engines.executor_config open public;
import arch.node.engines.executor_messages open public;
import arch.node.engines.executor_environment open public;
import arch.node.engines.executor_behaviour open public;
import arch.node.types.anoma as Anoma open;

open executor_config_example;
open executor_environment_example;

Executor Engine¶

The Executor Engine is responsible for executing transaction programs in Anoma, serving as the computational core that processes state transitions within the system. It operates as part of a distributed execution system, working in concert with Shard Engines that manage state access and Mempool Worker engines that take orders and spawn Executor engines based on those orders. Each Executor Engine instance is spawned to handle the execution of a single transaction in the form of a program which it is spawned with, making them ephemeral components that exist solely for the duration of their assigned transaction's lifecycle.

At its core, an Executor Engine receives read responses from shards and uses these to step through the transaction program's execution. Each transaction program defines a sequence of operations that may read from or write to various keys in the system's state. The Executor doesn't directly access this state - instead, it coordinates with Shard engines that manage actual state access.

The primary interface for the Executor Engine consists of three main message types that facilitate its operation. It receives ShardMsgKVSRead messages from Shards containing the data for requested state reads. For each read, the Executor applies this data to advance the transaction program's execution, potentially generating new read requests (ShardMsgKVSReadRequest) or write operations (ShardMsgKVSWrite) that are sent to the appropriate Shards. Once execution is complete, it sends an ExecutorMsgExecutorFinished message to both the Worker that spawned it and the transaction's issuer, containing a summary of all reads and writes performed during execution.

Engine components¶

• Executor Messages
• Executor Configuration
• Executor Environment
• Executor Behaviour

The type for an executor engine¶

ExecutorEngine : Type :=
  Engine
    ExecutorCfg
    ExecutorLocalState
    ExecutorMailboxState
    ExecutorTimerHandle
    ExecutorActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Example of an executor engine¶

exampleExecutorEngine : ExecutorEngine :=
  mkEngine@{
    cfg := executorCfg;
    env := executorEnv;
    behaviour := executorBehaviour;
  };

where executorCfg is defined as follows:

executorCfg : EngineCfg ExecutorCfg :=
  mkEngineCfg@{
    node := Curve25519PubKey "0xabcd1234";
    name := "executor";
    cfg :=
      mkExecutorCfg@{
        timestamp := 0;
        executable := "";
        lazy_read_keys := Set.empty;
        eager_read_keys := Set.empty;
        will_write_keys := Set.empty;
        may_write_keys := Set.empty;
        worker := mkPair none "";
        issuer := mkPair none "";
      };
  };

executorEnv is defined as follows:

executorEnv : ExecutorEnv :=
  mkEngineEnv@{
    localState :=
      mkExecutorLocalState@{
        program_state :=
          mkProgramState@{
            data := "";
            halted := false;
          };
        completed_reads := Map.empty;
        completed_writes := Map.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };

and executorBehaviour is defined as follows:

executorBehaviour : ExecutorBehaviour :=
  mkEngineBehaviour@{
    guards := First [processReadGuard];
  };