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¶

The executor engine is designed to be "agnostic" to choices of virtual machines and data formats, assuming only that the executable will run step by step (possibly involving program state updates) and interaction with replicated state machine state is via a key value storage interface.

ExecutorEngine (KVSKey KVSDatum Executable ProgramState : Type) : Type :=
  Engine
    (ExecutorCfg KVSKey Executable)
    (ExecutorLocalState KVSKey KVSDatum ProgramState)
    ExecutorMailboxState
    ExecutorTimerHandle
    ExecutorActionArguments
    (Anoma.PreMsg KVSKey KVSDatum Executable)
    (Anoma.PreCfg KVSKey KVSDatum Executable)
    (Anoma.PreEnv KVSKey KVSDatum Executable ProgramState);

Example of an executor engine¶

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

where executorCfg is defined as follows:

executorCfg : EngineCfg (ExecutorCfg String ByteString) :=
  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 {KVSKey KVSDatum} : ExecutorEnv KVSKey KVSDatum String :=
  mkEngineEnv@{
    localState :=
      mkExecutorLocalState@{
        program_state := "";
        completed_reads := Map.empty;
        completed_writes := Map.empty;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };

and executorBehaviour is defined as follows:

instance
dummyRunnable : Runnable String String ByteString String :=
  mkRunnable@{
    executeStep := \{_ _ _ := error "Not implemented"};
    halted := \{_ := false};
    startingState := "";
  };

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