Kairos

What Kairos is

Kairos belongs to the Janus family. Every command has a well-defined inverse, and uncall runs a procedure backwards. The reversible core (assignments, if … fi, from … until, local … delocal, call/uncall) follows Janus one to one. On top of it Kairos adds parallel blocks (par … and … rap), synchronous channels with channel passing in π-calculus style, stacks, arrays and a try … rollback … yrt construct.

The frontend is written in Python (PLY) and produces a textual bytecode. A VM written in C interprets that bytecode both forwards and backwards. You can run programs in this page: the same frontend and VM run in your browser.

The language

Types

Commands and their inverses

The variable on the left of an assignment must not occur in e, otherwise the assignment would lose information: x += x is rejected. Expressions support + - * / %, comparisons, && and || (both operands are always evaluated) and array cells.

local and delocal

As in Janus, local … delocal is a block. Each delocal closes the most recent open local of the same statement list and states the value the variable must hold at that point; the VM checks it. Outside main every variable is declared this way.

local int x = 0
local int y = x          // starts from the current value of x
...
delocal int y = x        // y must still equal x
delocal int x = 0

Conditionals and loops

if <entry guard> then
    ...
else
    ...
fi <exit assertion>

from <entry guard> do
    ...
loop
    ...
until <exit guard>

The fi assertion must be true after then and false after else. When running backwards it tells the inverse which branch was taken. A from guard must be true on entry and false every time the loop comes round again (LoopError1 and LoopError2). then, else, do and loop can be omitted.

Procedures

Parameters are passed by reference, and the arguments of one call must be distinct variables. Every program has a procedure main(). uncall p runs p backwards: the commands in reverse order, each replaced by its inverse. For recursive procedures the frontend compiles an inverse body p__inv.

Parallelism and channels

par
    ssend(<x>, c)
and
    srecv(<y>, c)
rap

Each branch of a par runs in its own thread, and the block ends when all branches end. Channels are synchronous: ssend waits for an srecv. Sending empties the source, and receiving requires a zeroed destination. A payload can hold ints, stacks and channels (endpoint passing). Inside a par each channel is a binary session used by exactly two branches with complementary protocols.

Branches share no writable memory. The frontend rejects an int or array written in one branch and used in another, also through called procedures. Branches communicate only through channels.

try … rollback … yrt

try x == 7          // commit condition, evaluated after the body
    x += 5
rollback            // optional
    x += 99
yrt x == 7          // exit assertion

If the condition holds after the body, the body is kept. Otherwise the body is undone by running it backwards, and the rollback runs. The yrt assertion must be true after a commit and false after a rollback, like the fi of an if. A try may not contain par or channel operations.

Output

show(x) prints x: value for any type, and show(x, char) prints the low byte of x as a character. show is its own inverse, so an uncall prints again, in reverse order. When the program ends the VM prints the variables of main after === VM dump ===.

Try it

Pick an example, edit it if you like, and press Run. The first run downloads the Python runtime that hosts the frontend (about 10 MB), so it takes a few seconds; later runs are immediate. Start from Blank to write your own program.

Output appears here.

More programs, including the ones that must be rejected, are in examples/, tests/ and test_error/.

Common errors

The full list of static and run-time checks is in the README.

Install locally

One line installs the right package for your distribution (.deb, .rpm or Arch) and asks for the sudo password:

curl -fsSL https://github.com/nicologiuliani6/kairos/releases/latest/download/install.sh | bash

You can also download a package from the releases and install it by hand. The packages contain a standalone frontend and the VM, so you don't need Python.

Then:

kairos program.kairos                  # compile and run
kairos program.kairos --dump-bytecode  # also write the bytecode to bytecode.txt

From source

You need gcc, make and Python ≥ 3.10 with venv.

git clone https://github.com/nicologiuliani6/kairos.git
cd kairos
make install-deps                     # venv + ply
make                                  # builds build/libvm.so
make run FILE=examples/fib.kairos

make test runs every program in tests/ and examples/. make test-error checks that each program in test_error/ is rejected with the error it is tagged with.

Debugger and related tools

• kairos-vscode-debugger: a VS Code debugger with Step Back and Reverse Continue. A step back runs the inverse of the previous instruction inside the VM. Install: curl -fsSL https://github.com/nicologiuliani6/kairos-vscode-debugger/releases/latest/download/install.sh | bash
• Mnemo compiles a subset of C to Kairos.
• The thesis covers the design and semantics of the language.

Questions

Open an issue on the repository, or email me@nicologiuliani.site.