DATE: 1 OCT 2015

Exe Language

TL;DR — certified executional environment of sequentional evaluations in process calculus on raw hardware.


Developing theory, model and implementation of minimalistic certified executive environment for a full application stack of components: hardware abstraction, language, virtual machine, message queue, database, HTTP and websocket servers, web application framework etc that is normalized for mass data usage, correct by construction and is usable today. Starting from underlying formalisms such as process and lambda calculus, temporal logic, type theory through virtual machine abstraction to the raw hardware, real world applications and protocol stacks ending up with samples, frameworks and documentation.

Keywords: Unikernel, Full-stack, Specification, Formal Methods, Certification, Event Streaming, Time Series, Protocol Analysis, Statistics.

The Idea and its space

Exe Language is an attempt to formally specify and validate the inter-component communications using such tools TLA+ — a model checker for distributed systems. But Exe is not limited to temporal logic, it also provides type theoretical notation, graphical language based on Petri Nets, inner semantics of pi-calculus. Here is the list of theories Exe Language can be expressed in:

and other types of foundations for easier and more effective



Linearizability is a key feature in one to many relation, storing the sequences, iterators and execution logs. Vector of two elements can encode binary trees and confluent case — lists.

The main trick is the lists is best to encode the sequence of execution, data parameters, code itself, and are easy to store in KV stores. The linear nature of executions helps in such protocols as XA, Chain Replication and RETE matching. The lists are also a foundation to virtual machine's messaging queues and other core data structures.

Iterator over Chain

Behavior of Time Series

According to TLA+ behaviors is the chronological sequence of states. This is the basic representation of process protocols, iterators and other chain based data. For statistical software like R or Julia you also need to provide your data as a time series of some state. Seems like treating any data as arrays of records is the best way to handle it. The fact that the event stream has a constant record in its base us to the domain of monoidal actions.

The other goodie about recorded event stream is that system can be replayed starting from initial system state similar to how it's happens in log-based replicated databases. This opening the space to distributed consistent transactions streams such as CR and TPS.

Recorded Event Stream

Λ : ⊗ Ι Λ Μ Ο Σ | Ξ

The iteration of system or protocol messages is taken as recorded behavior of the system. The iteration of data messages is taken as persistent feeds. The system itself consist of different protocol bands which are tuples definitions. These protocol bands called applications and the overall system state is just zip of protocol bands which are given in application band signature list.

Algebraїc Approach

By using algebraic language we could describe linearized process with semgroup actions, which was previsous successfully used for modeling FSM automatas.

Α : Σ · Φ → Φ action protocol state -> state Φ : Λ ⊗ Σ state = { history, protocol } Λ : Σ ⊗ Φ ⊗ Λ history = { protocol, state, history } | Ξ | [] Σ : message ⊗ _ protocol = { message, _ } | event ⊗ _ | { event, _ } | call ⊗ _ | { call, _ } | Ξ | []

Inversable Actions

Having reversavle function will allow us to reconstruct the state of the process, which is usually much bigger than a messages, on only by direct function but also by inverse function. Natural support for inversable actions provided by doubly-linked lists which also has a signature equals to binary trees.

st(p) = p(st-1) — applying state to protocol function

p-1(st) = st-1 — reverse step

Φ : ⊗i Λ : ⊗ Ι Φ Λnext Λprev | Ξ

Lightweight Unikernel Environments

During the years various computer systems designs were changed and not all good theories were met with good implementations. From the ancient full-stack Lisp Machines, Smalltalk virtual machine which was able to transfer their state on different platform, and modern executional platforms like managed object-oriented CLR, functional Haskell and Erlang. At the base however you still observe UNIX or Windows NT based executional environments which is far from being verifiable and correct moreover they consume more power because of layering the abstractions. Languages like Erlang, Haskell and OCaml are most suited for the further eveloving of correctness and provability. They provide LING, HaLVM and Mirage lightweight unikernels respectively.

If you ask me to find other words to describe this work I would say that this work is an attempt to build close to theoretical adequate and precise executional environment that is easy to be verified and managed, encoded in most effective way, optimized by defition and construction, that relies close to hardware and provides top level modern software language access in Erlang.

Constructing the Specfication Language


• Ease of expressing constructs arising in problems.
• Suggestivity.
• Ability to subordinate detail.
• Economy.
• Amenability to formal proofs.
• Isomorphic Visual and Algebraic languages.

Exe Legend and Petri Process sample

We will extent Petri nets graphical language alphabet with several letters up to seven. This language preserve message-passing semanthics along with core primitives such as client or server process, feed chains or indexed tables (B+,B*). We will use this language also to define the signatures of top-level applications.

Virtual Machine

action is the piece of code applied to message using pattern matching.
record is the tuple that defines a protocol.
client is the true customer of the system who is using service on daily basis.
server is the process nicely scheduled by the system.
feed is the server managed list of records.
table is the ixset or ets based queryable tables.


app is the web clients monoidal state machine.
proc is the oriented graph monoidal executional engine.
store is the 2-category key-value database.


ok1 : OK ⊗ _ error1 : ERROR ⊗ _ io2 : IO ⊗ _ ⊗ _ action2 : EV ⊗ _ ⊗ _ | INIT ⊗ _ ⊗ _ | TERM ⊗ _ ⊗ _ | HANDLE ⊗ _ ⊗ _ | ACTION ⊗ _ ⊗ _ elementi : HTM | BOD | MET | H1 | TAB | ... fieldi : BIN | INT | TUP | LST | OPT | SEL recordi : ⊗i table1 : ⊗1 record document1 : ⊗i field process0 : ⊗5 action2 [ task ] ⊗2 task task [ document ] cx3 : ⊗3 action2 actions container3 : ⊗3 action2 top count


bintree1 = Λ2Φ : Ξ | ⊗4 Ι Φ Λn Λp list1 = Λ1Φ : Ξ | ⊗3 Ι Φ Λn scalar0 = Λ0Φ : Ξ | ⊗2 Ι Φ Δ Λ0 : ⊗0 Δ Λn : Λn-1 api1 : ⊗6 spawn get push fold ev3 : ⊗4 τ Ω message ⊗2 source target tx3 : ⊗4 τ Ω payload ⊗2 subsidiary beneficiary relations : table1 entry | [ entry ] | feed3 user feed entry


2005 2013 2013 2015
BPE = ⊗1 event _ | ⊗1 push _ | Ξ N2O = ⊗2 io _ _ | ⊗1 ok _ | ⊗1 error _ | ⊗1 client _ | Ξ KVS = ⊗0 get | ⊗1 put _ | ⊗1 add _ | ⊗1 remove _ | Ξ MQS = ⊗2 sub _ _ | ⊗1 unsub _ | ⊗2 pub _ _ | ⊗3 msg _ _ _ | Ξ


session1 : ⊗4 Λev cx WEB api proc1 : ⊗4 Λhistory process ACT api account1 : ⊗4 Λtx customer TPS api feed1 : ⊗4 Λiterator container DBS api


store3 : ⊗6 Λid_seq Λtable Λfeed kvs KVS api roster2 : ⊗5 Λfeed [ Λfeed ] [ table ] ROSTER api app2 : ⊗5 Λsession Λproc [ table ] N2O api depot1 : ⊗4 Λaccount [ table ] XA api act1 : ⊗4 Λproc [ table ] BPE api

Application Band Signatures

Business Process

Picture 1. BPE Application 1 Category


Picture 1. KV Application 2 Category

Application Server

Picture 1. N2O Application 1+1 Category

Message Queue

Picture 1. One-to-one and one-to-many channels with coordination tables


Picture 1. Chat Application

Distributed Transactions

Picture 1. The example with VNode hashring of 64 on a cluster with 3 nodes

Satisfaction Landscape

Whenever customer is being satisfied this joy is always fall into the following categories:

Technical Landscape:

Target areas:




Compact, adequate and precise typed executional environment for the OSI stack. Compact enought for quick check. Adequate enough to theorethical models.


The end result of the project is a complex thing that should in its fullness consist of: