Spacetime Programming

Spacetime programming is a programming language on top of Java to describe search strategy when exploring a state-space, for example in constraint satisfaction problems. Spacetime started as a research project and is formally described in this dissertation. A Java project integrating spacetime code can be set up in 5 minutes with the Maven build system.

Spacetime is based on two main paradigms: synchronous programming and concurrent constraint programming (CCP). These two paradigms are not mainstream and it is very likely that you did not hear about these two paradigms before. In this tutorial, we walk you through the syntax and semantics of spacetime with various examples. Our goal is to keep the tutorial accessible to programmers and computer scientists, and to give you an idea of the kind of problems this language can solve.

Independently of your background, a first step is to read the Getting Started chapter. We introduce the concepts of Synchronous Programming and the syntax of spacetime through several small examples. We make sure the build system is working out for you. Secondly, we introduce some novelties of Spacetime Programming with examples stemming from constraint satisfaction problems such as Sudoku. We next consider the more advanced concept of Universe which is useful to design restarting search strategies. Finally, we go through a full application of this language by designing a interactive search strategy for an application of musical composition.

The code is available on github.

Note that this tutorial is a work-in-progress.

Syntax cheat sheet

p and q are statements, e is an expression, x a variable identifier and st is a spacetime attribute (either single_space, single_time and world_line).

Statements Description
st T x = e Declares the variable x of type T with the spacetime st.
when e then p else q end Executes p if e is equal to true, otherwise q.
x <- e Joins the information of e into x.
o.m(x1,..,xn) Executes the Java method m on the object o. Variables must be annotated by read, write or readwrite (read by default).
pause Delays the execution to the next instant.
pause up Delays and gives the control back to the upper universe.
stop Delays and gives the control back to the host language.
par p||q end Executes concurrently p and q. Terminates when both terminate.
par p <> q end Same as || but terminates in the next instant if one process terminates before the other (weak preemption).
p ; q Executes p, when it terminates, executes q.
loop p end Executes indefinitely p. When p terminates it is executed from its beginning again.
space p end Creates a new branch. All world_line variables are copied and are modified by p when the node is popped.
prune Indicates that a branch should be pruned.
abort when e in p end Executes p unless e is true, in which case the statement terminates in the current instant.
suspend when e in p end Executes p in every instant in which e is false.
universe with x in p end Executes p in a universe with the queue x.

Getting Started

The project is decomposed into two parts:

  • Bonsai is the compiler of the Java extension and is written in Rust.
  • Bonsai runtime is the Java runtime used by the code compiled by bonsai.

We provide instructions to install both as well as their dependencies.

Prerequisites
  • rustup: curl https://sh.rustup.rs -sSf | sh (do not forget to source your profile).
  • Maven, it is usually available in the package manager of your distribution:
    1. MacOSX: sudo brew install maven
    2. Linux Ubuntu: sudo apt-get install maven

Installation

You need to install both the compiler and the runtime using the setup.py script.

git clone https://github.com/ptal/bonsai.git
cd bonsai
python3 setup.py

We provide a manual installation procedure below in case the script did not work.

Update

Update the compiler and runtime (without the external libraries such as Choco):

./update.sh

Uninstallation

 
cargo uninstall bonsai
# Remove runtime in the Maven local database
rm ~/.m2/repository/bonsai

Manual installation

Step-by-step installation of the bonsai compiler and its runtime. Before attempting the manual installation, you should try the setup.py script as described above.

  1. Install prerequisites: same as above (rustup and Maven).
  2. Installing the bonsai compiler:
rustup override set nightly-2018-11-09
cargo install

You can verify everything is working by running bonsai --help in your terminal.

  1. Installing Bonsai standard library: The standard library provides several modules to ease the development of Bonsai application.
cd libstd # (inside the bonsai repository)
./install.sh
  1. Installing the Bonsai runtime: The Bonsai runtime has a dependency on Choco for constraint programming. Choco will be downloaded automatically from the Maven central repository. However, we need to install the Bonsai runtime in the local Maven database:
cd runtime/ # (inside the bonsai repository)
./install.sh

That's it! You should be ready to go to the next section.

Learn Spacetime

Please install spacetime first to run the program of this section.

Running a first program

In this section, we compile a first spacetime program in a Java project. Go to the toy project available at examples/bonsai/HelloWorld and launch the following script:

./run.sh

It compiles and runs the code. It prints the message HelloWorld 5 times:

Hello world!
1
Hello world!
2
Hello world!
3
Hello world!
4
5

You can start from this code to modify it. The standard library of spacetime is usable and you can find different modules in the directory libstd.

Universe

Application: Musical Composition

Companion guides to research papers

For each paper written about spacetime, I maintain a companion guide in order to:

  1. Provide instructions to install the exact same version of the language than the one used in the paper.
  2. Help people who wants to execute the examples presented in the paper.
  3. Replicate the benchmarks with a single command.

Companion guide (PPDP19)
  • Reference: P. Talbot, “Spacetime Programming: A Synchronous Language for Composable Search Strategies,” in Proceedings of the 21st ACM International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), Porto, Portugal, 2019.
  • The paper is available here.
  • Tagged version of the language used in the paper on Github.

This supplementary material gives instructions to compile and run the examples and benchmarks presented in the paper.

Prerequisites
  • rustup: curl https://sh.rustup.rs -sSf | sh (do not forget to source your profile or restart your terminal).
  • Maven, it is usually available in the package manager of your distribution:
    1. MacOSX: sudo brew install maven
    2. Linux Ubuntu: sudo apt-get install maven

Installing Bonsai (tag PPDP19)

If you want to replicate any benchmark and running examples, first install the compiler and runtime as follows:

git clone https://github.com/ptal/bonsai.git
cd bonsai
git checkout PPDP19
python3 setup.py

If you have any issue, please consult Getting Started for further instructions.

Demo of the examples in the paper

We provide a demonstration of the programs given in the paper in the directory PPDP19. After installing spacetime, you can simply type:

cd examples/bonsai/PPDP19
./run.sh

Additional examples of strategies

Examples are provided in the standard library of spacetime. In particular, we have the following:

How to run the benchmark

After installing spacetime, you can simply type:

cd benchmark
./run.sh

The file Benchmark.java contains some parameters that can be tweaked such as the size of the instances.

Tests

The compiler and runtime of spacetime are well tested, you can run the tests of the compiler with:

cargo test
cd runtime
mvn test

There are about 200 tests, ranging from the static analysis of the compiler (compile-fail and compile-pass), to the runtime behavior (run-pass), and the correctness of the lattice library.

Contributing