Skip to content

utahplt/programming2025_artifact

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

20 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Artifact for Chorex

Key metadata:

Overview

This artifact provides running code that support the claims made in the paper. The programs herein demonstrate various features of Chorex as well as some performance characteristics.

This artifact is available as source code and as a Docker container.

We recommend running the Docker container, as it includes all the dependencies necessary.

Claims supported

  • §1, Figure 1: IDEs integrate with Chorex
  • §1: Chorex catches crashing actors
  • §1: Chorex reports deadlocks as compiler errors
  • §2.1: Demo of a TCP socket handler
  • §2.2: Demo of the SRP protocol
  • §2.3: Demo of a discrete-logarithm ZKP protocol
  • §2.4: Chorex supports higher-order choreographies
  • §4, Figure 7: Chorex projects receives into separate functions
  • §5, Table 1: Performance overhead of using checkpoint/rescue

Getting started

Prerequisites

You will need Docker to run this artifact.

Steps

  1. Ensure that a container runtime is running. Run $ docker ps and it will tell you if it's not.

  2. Pull the artifact container:

    For Apple M-series processors, use this image:

    docker pull researcherw/chorex-artifact:latest

    or use the arm64 tar file from Zenodo and unpack:

    curl -O https://zenodo.org/records/16783343/files/chorex-artifact-container-arm64.tar.gz?download=1
    docker load -i chorex-artifact-container-x86.tar.gz

    For x86 architectures, use this image:

    docker pull researcherw/chorex-artifact:x86_latest

    or use the x86 tar file from Zenodo: (note the changed file name!)

    curl -O https://zenodo.org/records/16783343/files/chorex-artifact-container-x86.tar.gz?download=1
    docker load -i chorex-artifact-container-x86.tar.gz
  3. Start the container:

    docker run --rm -it researcherw/chorex-artifact bash
  4. Inside the container, run kick_tires. This will verify a subset of the claims and should run quickly. At one point a code listing will appear; use j/k or the arrow keys to scroll as you would with the less program, and type q to quit. The rest of the kick_tires phase should run without intervention.

Step-by-step instructions

Start the docker container:

docker run --rm -it researcherw/chorex-artifact bash

Once inside the Docker container, you can run some of the scripts all together with push_button. This script supports several, but not all of the claims.

All these commands should be loaded into the shell's environment at startup. You can find them inside runner.sh.

For further help, run artifact_help to see a list of artifact-related commands that you can run.

Extra container features

We have set up the container with a few utilities to make investigating the artifact easier:

  • l this is an alias for ls -la
  • bat this is a pager like cat but it has syntax highlighting; do bat foo.ex to get a nice view of the contents of foo.ex

IDE error reporting and integration (§1, Figure 1)

Command: ide_claims

Demonstrates that a text editor (in this case, Emacs) can interface with the Elixir language server to accurately report error information and provide suggestions to implement actors.

Running ide_claims will open up Emacs and start the language server for a project. Please wait for the language server to start before continuing. This should take a few seconds; once it's up and running, you will see eglot:ide_demo appear in the mode line at the bottom of the screen. Follow the instructions in the comment blocks in the file.

Deadlock reporting (§1)

Command: deadlock_claim

Code location: /root/claims/deadlock_claim/lib/deadlock_claim.ex

Demonstrates that writing down a deadlock scenario gets caught by the Elixir compiler as an undefined variable error.

Running the command attempts to compile a small mix project that uses Chorex and describes a simple deadlocking system. mix should report a compile error about an undefined variable x. Moreover, the error should be reported in terms of the source syntax, and should not show any macro-expanded code.

Basic error recovery (§1)

Command recover_claim

Code location: /root/claims/chorex_examples/deps/chorex/test/mini_fail_test.exs

Runs a test from the Chorex test suite checking that basic failures like those demonstrated in §1 are caught.

You should see 2 tests, 0 failures in the output.

Secure Remote Password (§2.2)

Command srp_claim

Code location: /root/claims/chorex_examples/lib/mix/tasks/demo/srp.ex

Runs the SRP protocol. No further interaction required; the script will print messages with directions on what to look for.

Discrete Logarithm ZKP (§2.3)

Command zkp_claim

Code location: /root/claims/chorex_examples/lib/mix/tasks/demo/zkp_log.ex

Runs the logarithm-based ZKP. No further interaction required; the script will print messages with directions on what to look for.

Higher-order choreographies (§2.4)

Command hop_claim

Code location: /root/claims/chorex_examples/deps/chorex/test/higher_order_test.exs

Runs a higher-order choreography from Chorex's test suite. You should see a message saying 3 tests, 0 failures.

Projection example (§4, Figure 7)

Command projection_claim

Code location: /root/claims/chorex_examples/projection_example.ex

Use j/k or the arrow keys to scroll up and down, and type q to quit.

Macroexpands a small choreography like the one seen on the left side of Figure 7 and pretty-prints the result.

Look for the projection of the Bob module: you should see a handle_continue function matching the green box on the bottom of the right side of the figure, and the run function like that in the red box.

Observe that the string in the call to push_recv_frame matches the string matched in the function head of handle_continue. (The script should highlight the call to handle_continue on line 76. Look for the corresponding token on line 111.)

Note that we took some liberties with the syntax in the diagram to make it fit. The essential point is that a receive gets split across different functions in a GenServer and they are tied together with a unique token.

Performance overhead (§5, Table 1)

Command performance_benchmarks

Code location: /root/claims/chorex_benchmarks

Relation to paper:

  • State Machine: look for state machine (chk) and state machine (chk+recover)

  • Mini BlockChain: look for miniblock (chk) and miniblock (chk+recover)

  • Flat-10k: look for flat loop 10k itrs (chk) and flat loop 10k itrs (chk+recover)

  • Nest-1k: look for nested loop 1k itrs (chk) and nested loop 1k itrs (chk+recover)

  • Nest-10k: look for nested loop 10k itrs (chk) and nested loop 10k itrs (chk+recover)

Numbers reported will have some minor variance from the paper. Running all the benchmarks should take a little over 5 minutes.

TCP Socket Handler (§2.1)

Command: tcp_claim

Code location:

  • /root/claims/chorex_examples/lib/tcp_server.ex (Application root)
  • /root/claims/chorex_examples/lib/tcp/listener_chor.ex (Choreography for listening on a port)
  • /root/claims/chorex_examples/lib/tcp/handler_chor.ex (Choreography for each connection)

Run tcp_claim in the Docker container. This will print out some instructions to connect to the already-running container. Run the command and change the hash to match:

# This hash will be different: use what the logger spits out

$ docker exec -it bf5acff7a873 bash

Now that you've connected to the container, connect to the port:

$ nc 127.0.0.1 4242

After running the command, type a phrase like hello world and press enter. You should get a message back from the server counting how many bytes in your last message and a running total over subsequent messages.

You can optionally connect in a third terminal window by running the same docker exec command and connecting to the same port:

$ nc 127.0.0.1 4242
what's up?

You should get messages back from the server, and the running totals should be separate for each session.

Back in the Docker container, observe that the server is logging the messages as they arrive.

About

Artifact for Chorex at Programming 2025

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published