# The Linear Session Abstract Machine (Artifact, June 2025 version)

This document describes the companion artifact for the ESOP
paper `The Session Abstract Machine`, and the current journal submission 
`The Linear Abstract Machine`.

The artifact consists of a type checker and an interpreter for 
the language of the Linear Session Abstract Machine (SAM) presented in
the papers.

The artifact is distributed as a Docker image that bundles the source
code, all its dependencies, the examples from the paper and several
other examples that showcase the abstract machine. 
 

Authors: Luís Caires, Bernardo Toninho.


[![CC BY 4.0][cc-by-shield]][cc-by]

This work is licensed under a
[Creative Commons Attribution 4.0 International License][cc-by].

[![CC BY 4.0][cc-by-image]][cc-by]

[cc-by]: http://creativecommons.org/licenses/by/4.0/
[cc-by-image]: https://i.creativecommons.org/l/by/4.0/88x31.png
[cc-by-shield]: https://img.shields.io/badge/License-CC%20BY%204.0-lightgrey.svg


## Getting Started Guide 

1. After uncompressing the supplied archive file, you should obtain a 
directory with the following contents: 

* `Dockerfile` -- Configuration file and setup script for the docker image.
* `README.md`  --  The readme file with instructions for getting started and step-by-step 
                   instructions to use the implementation. 
* `LICENSE.txt` -- Creative Commons Atrribution 4.0 International License. 
* `bin/` -- Folder containing the compiled Java .class files. 
* `examples/` -- Folder containing examples
* `lib/` -- Folder containing initial definitions loaded by the artifact. 
* `makeit` -- Build script.
* `SAM` -- Executable file to start the interactive REPL. 

2. You should have a Docker runtime installed, installation instructions are 
   available in https://www.docker.com. Ensure that the Docker daemon is running. 

3. Run the command `docker build --tag=sam .` to build a docker image tagged `sam`. Alternatively,
   run the command `docker load -i sam.tar` to load the pre-built image.
   

4. To run the docker image tagged `sam`, execute the command `docker run -it sam`. 
   This will start the image and its bash shell in a directory identical to the root of
   the artifact archive.

5. To run the artifact as an interactive REPL (inside the running docker image),
   execute `./Makeit` to build the artifact and `./SAM` to run the interpreter and typechecker. 
   For convenience, we have provided the file `examples/sam/sam-all.clls` 
   that type check and runs all the examples. 
   For example, to run all  examples defined in the paper you can execute 
   `include "examples/sam/examples-lsam.clls";;` or `include "examples/sam/paper-examples-sam.clls";;`  in the REPL. Note that many
 examples produce little visual output since they do not use the `print` or `println`
   statements.
   
6. To exit the REPL execute `quit;;`. To exit the docker image, execute `exit`.
    
## Step-by-Step Instructions 

The artifact consists of type checker and interpreter for the SAM, 
written in Java. The artifact is developed on top of the CLASS
interpreter and typechecker by Rocha and Caires (available [here](https://luiscaires.org/software/)).
The artifact supports the main language in the paper, with a few convenience extensions such
as type and process definitions, primitive *linear* integers, strings and booleans. 
Note that these primitive values are typed linearly and so must be used exactly once 
(a common idiom is to use them in print statements).
The interpreter supports execution in both reduction style (as described in Section 2 of the paper)
and using the execution rules of the SAM (as defined in Section 3 of the paper).
By default, processes are executed in reduction style. To execute a process in the SAM, use
the command `sam P;;` where `P` is a process.

In particular, all the examples presented in the paper are validated by the 
implementation. 

ackermann-sam.clls
bit-counter-sam.clls
examples-lsam.clls
naturals-sam.clls
paper-examples-sam.clls
recursion-for-free-sam.clls
sam-all.clls
sam-exponentials.clls
sam-forwarders.clls
sam-mult.clls
sam-sieve-sum.clls
sam-sums.clls
sam-units.clls

==

We will now present the commands to interact with the REPL and the concrete syntax
of the implementation language. We conclude with some final remarks. 

### Interacting with the REPL (read-eval print loop)

The examples below assume the same REPL session.

The REPL expects the following top-level commands:
	
	1. `type id{ A };;`
	2. `proc id(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };;`
	3. `P;;`
	4. `sam P;;`
	5. `trace L;;`  
	6. `include "filename";;`
	7. `quit;;` 
	
Command (1): top level type definition.

Defines (if it kindchecks) the type A with name id.

Example: when executing 
`type tmenu {
    offer of {
        |#Neg:  recv ~lint; send lint; close 
        |#Add:  recv ~lint; recv ~lint; send lint; close
    }
};;` we obtain  

>Type tmenu: defined.

(2) Defines (if it typechecks) the process 
with name id  with linear  parameters  x1:A1,..., xm:Am (m >0) and
unrestricted (exponential) parameters y1:B1,..., yk:Bk (k>=0).

The process is typechecked as defined by the typing judgment

P |- x1:A1,..., xm:Am ; y1:B1,..., yk:Bk

Example: if we type in the REPL
```
	proc client1( ; s:~tmenu){
    call s(c);
    #Neg c;
    send c (v:lint. let v 2);
    recv c(m);
    wait c;
	println("CLIENT1 GOT NEG = " + m);
    ()
};;
```
we obtain 

> Process client1: defined.  




Commands (3) and (4) type check process P in the current
environment given by prior definitions and execute it.

The  main focus of this artifact is (4),  which executes the process P
using the Session Abstract Machine semantics defined in the paper.

Command (3) executes the process using the multithreaded reduction
semantics previously developed for CLL.

Example: if we input in the REPL (usar o primeiro exemplo do paper ??)
```
	proc example1() {
	cut {
		send a(y. close y); println ("sent on a") ; close a 
		| a: ~ send close ; close |
		recv a(x); wait x; wait a; println ("Done with waiting");()
	    }
    };;
    sam example1();;

```
we obtain the log:

> sent on a
  Done with waiting

Command (5) enables tracing of the SAM execution with `trace 1` and disables it with `trace 0`. 
For instance, running `sam example1()` from above with `trace 1` active produces the output:

```
cut-op a SessionRecord@3a883ce7 size=2
send-op a SessionRecord@3a883ce7 @ 0
sent on a
clos-op a SessionRecord@3a883ce7 @ 1
recv-op a SessionRecord@3a883ce7 @ 0
clos-op y SessionRecord@4973813a @ 0
wait-op x SessionRecord@4973813a @ 0
wait-op a SessionRecord@3a883ce7 @ 1
Done with waiting
empty-op
```

Each line indicates the semantic rule that triggers at each step. In this example, following the rule
for cut, the send on a is executed, followed by the close on a. Each line also mentions the index into
the message buffer on the session record.


Command (6) includes and processes all the commands included
in the specified file. Filenames are given as strings.

Example: `include "examples/sam/sam-all.clls";;`. 

Command (7) quits the REPL. 
 
By convention, we use the filename extension `.clls` for files written in the 
implementation language.

Single-line comments are written as follows

```
//this is a single-line comment
``` 

whereas multiple-line comments are written as
```
/*
this is 
a multiple-line
comment
*/
```

### Concrete Syntax


#### Types 

The concrete syntax of types is given by: 

	A,B ::=

	lint |

	colint |

	lbool |

	colbool |

	lstring |

	colstring | 

	close |   ( 1 )

	wait |    ( bottom )

	send A; B |  ( A (x) B ) 

	recv A; B |  ( A (p) B ) 

	choice of {|#l1:A1 | ... |#ln: An} | ( (+){|#l1:A1 | ... |#ln: An} ) 

	offer of {|#l1:A1 | ... | #ln:An} | ( &{|#l1:A1 | ... |#ln: An} ) 

	!A |

	?A |

    ~A |  (negation = duality)

	
The correspondence to the types of the paper are written in parenthesis when not immediate. 
	         
Except for the basic type constants, concrete types correspond to those 
described in the paper. We have basic type constants for linear integers 
`lint`, linear booleans `lbool`and linear strings `lstring`, as well as their 
dual `colint`, `colbool` and `colstring`.  Unrestricted versions of
these types may be defined using ! and ? type constructors.

Choice label identifiers must start by a hash character`#`.

#### Processes

The concrete syntax of process terms is given by: 
	
    P, Q ::=

	print M; P |

	println M; P |
	
	if M { P }{ Q } |

	let x M |

	let! x M |
	
	id(x1, ..., xm) |
	
	() |

	par {P || Q } |    (P || Q)

	fwd x y |

	cut { P |x:A| Q } | 

	close x |

	wait x; Q |
	
	case x of {|#l1:P1 | ... | #ln:Pn} 
	
	| #li;Pi 
    
	send x(y:A. P); Q |

	recv x(y:A);Q |
	
	!x(y:A);P |

	call x(y:A);P | ?x; P |	        

	send x(M);P 
	
The correspondence to the processes of the paper are written in parenthesis when not immediate.

The first six constructs are basic extensions to the logical language to deal with values of primitive type.
Constructs `println M;P` and `print M;P` respectively print their (evaluated) 
argument expression `M` with or without an added new line, and then procceed as process `P`.
We also support a process-level `if` construct with the expected semantics (where both
the then and else branch processes must have the same typing) and auxiliary linear (`let x M`)
and unrestricted (`let! x M`) bindings of values to names (which must be accessed via a `cut`).
Such values must be either integers, booleans or strings (in their linear or unrestricted forms, respectively).

The concrete syntax of basic value expressions is given by:

	M :: =   n | true | false | str | x | (M) |
		    -M | M + M | M - M | M * M | M / M |
		    !M | M and M | M or M | 
		    M == M |  M != M | M < M | M > M 

where `n` is any integer, `true` and `false` denote the boolean constants, 
`str` is any string and `x` is an identifier. We support the usual arithmetic operations 
of negation, addition, subtraction, multiplication and division. We support 
the boolean constructs of logical negation `!`, logical `and` and logical `or`. 
We can compare two expressions for value equality `==` and non-equality `!=`. 
We can compare two integers with the usual relational operators "<" and ">".
The operator of addition `+` is overloaded: we can concatenate two string
expressions, obtaining a string. We can also concatenate a string with an 
integer expression, in which case, the integer is first converted to a string.

Construct `id(x1,.. ; .,xm)` spawns the 
defined process `id` with channel name arguments `x1,..; .,xm`. The `;` in the
argument list separates the linear parameters from the unrestricted
parameters, according to the definition of `id`.
 
For convenience, our concrete syntax supports multi-ary independent parallel composition and
multi-ary cut (which are abbreviations of the expected associative
composition of parallel and cut). 

`par {P1 || ... || Pn}`
`cut { P1 |x1:A1| ... |xn:An| Pn+1}`

Multi-ary cut associates (conventionally) to the right.  
Access to exponential names is inferred by our type checker and 
so we omit the `cut!` construct from the paper.

### Some Remarks

In our concrete process syntax terms are written with bound 
names type-annotated, which from a pragmatic point of view guides the
type checking algorithm and eases the task of writing programs.
Currently, inference of annotations is provided, so that
only  parameters in process definitions and cut bound names need to 
be explicitly type annotated.

We also note that since our syntax is that of CLL and so `cut` introduces only one 
name, shared by both processes. The type `A` in `cut { P |x:A| Q }` refers to the 
usage of channel `x` according to process `Q` (and so `P` uses `x` according to type `~A`).
This is flipped from the convention in the paper.

Our SAM proof-of-concept implementation is build using the JDK, on top
of the CLASS infrastructure  (see website linked above). 

The implementation follows the structure of a virtual machine
interpreter that adheres to the
environment-based semantics described in Section 3 of the paper. The top
execution loop starts in `SAM.java`, which calls the `samL()` method for
each
instruction: given a machine state, it executes the next instruction, and
returns the next machine state (essentially a pair (continuation,
env1, env2), where env1 is is the (linear) runtime environment (a spaghetti
stack) and env2 is a global enviroment storing process definitions. 

The implementation of the virtual machine covers all the (sequential) constructs in
the paper, and also basic polymorphic constructs (not discussed in the paper, 
but exemplified e.g. in the recursion-for-free-sam.clls example).

To establish a tighter correspondence with compilation techniques that
we plan to develop in future work, we  represent each session queue 
with a low level array-based imperative structure, akin to a stack frame in a funcional
language, allowing linear values to  passed in sessions. Thus, in our
case, session records behave as a kind of co-routine frames,
paving the way for very efficient execution strategies. The size of
such so-called SessionRecords is statically computed from the session
type. We are currently extending the SAM to handle recursive types,
concurrent constructs and mutable state (cf. [58,59]).

To inspect the sequence of instructions executed by the SAM whle
running a program we may switch tracing mode on using the 
following REPL command.

> trace 1;;

Tracing may be switched of with

> trace 0;;

Each line of a trace starts by the current instruction (as in the
code component of the SAM), we also indicate the channel name, the
respective SessionRecordid (as a JVM object) and the session record slot
being written or read.
The instructions tagged by [S-] correspond to the [S-] execution
of the SAM (see Figure 5) in the paper. 






