PROCESS MODALITY

Process Calculus defines formal business process engine that could be mapped onto Synrc/BPE Erlang/OTP application or OCaml Lwt library with Coq.io front-end. Here we will describe an Erlang approach for modeling processes.

We will describe process calculus as a formal model of two types: 1) the general abstract MLTT interface of process modality that can be used as a formal binding to low-level programming or as a top-level interface; 2) the low-level formal model of Erlang/OTP generic server.

According to MLTT, declaring a type means formally defining its formation rule or type former, sole introduction rule, a lot of elims (projections and modality morphisms, recursor, and induction), and beta and eta computational equalities. In this article we will formally define process modality and will end up with two examples: Erlang/OTP generic server process and Synrc/BPE application.

MODALITY

Definition (Storage). The secure storage based on verified cryptography. NOTE: For simplicity let it be a compatible list.

storage: U -> U = list

Definition (Process). The type formation rule of the process is a $\Sigma$ telescope that contains: i) protocol type; ii) state type; iii) in-memory current state of process in the form of cartesian product of protocol and state which is called signature of the process; iv) monoidal action on signature; v) persistent storage for process trace.

process : U
    = (protocol state: U)
    * (current: prod protocol state)
    * (act: id (prod protocol state))
    * (storage (prod protocol state))

Definition (Spawn). The sole introduction rule, process constructor is a tuple with filled process type information. Spawn is a modal arrow representing the fact that process instance is created at some scheduler of CPU core.

spawn (protocol state: U) (init: prod protocol state)
      (action: id (prod protocol state)) : process
    = (protocol,state,init,action,nil)

Definition (Accessors). Process type defines following accessors (projections, this eliminators) to its structure: i) protocol type; ii) state type; iii) signature of the process; iv) current state of the process; v) action projection; vi) trace projection.

protocol  (p: process): U = p.1
    state     (p: process): U = p.2.1
    signature (p: process): U = prod p.1 p.2.1
    current   (p: process):          signature p  = p.2.2.1
    action    (p: process):      id (signature p) = p.2.2.2.1
    trace     (p: process): storage (signature p) = p.2.2.2.2

NOTE: there are two kinds of approaches to process design: 1) Semigroup: $P \times S \rightarrow S$; and 2) Monoidal: $P \times S \rightarrow P \times S$, where P is protocol and S is state of the process.

Definition (Receive). The modal arrow that represents sleep of the process until protocol message arrived.

receive (p: process) : protocol p = axiom

Definition (Send). The response free function that represents sending a message to a particular process in the run-time. The Send nature is async and invisible but is a part of process modality as it's effectfull.

send (p: process) (message: protocol p) : unit = axiom

Definition (Execute). The Execute function is an eliminator of process stream performing addition of a single entry to the secured storage of the process. Execute is a transactional or synchronized version of asynchronous Send.

execute (p: process) (message: protocol p) : process
  = let step: signature p = (action p) (message, (current p).2)
    in (protocol p, state p, step, action p, cons step (trace p))

Applications

1) Run-time formal model of Erlang/OTP compatible generic server with extraction to Erlang. This is an example of low-level process modality usage. The run-time formal model can be seen here: streams.

2) Formal model of Business Process Engine application that runs on top of Erlang/OTP extracted model. The Synrc/BPE model can be seen here: bpe.

3) Formal model of Synrc/N2O application and n2o_async in particular.