-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
1 changed file
with
57 additions
and
47 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,53 +15,6 @@ Set 1 requires Linux x86_64 (Ubuntu 22.04) with at least 8 physical cores on one | |
|
|
||
| Set 2 requires a Windows x86_64 machine with .NET 5 or newer (we tested .NET 8.0), rust 1.76.0, and python 3 (we will provide installation instructions). A reasonably recent laptop or desktop should be sufficient. | ||
|
|
||
| To run this experiment, take the following steps: | ||
|
|
||
| * Build the IronFleet version of IronSHT. | ||
| * Install `dotnet`. | ||
| * Install `scons` with `pip install scons`. | ||
| * Download the Dafny 3.4.0 release, including its executable, from | ||
| `https://github.com/dafny-lang/dafny/releases/download/v3.4.0/dafny-3.4.0-x64-win.zip`. | ||
| * Sync to commit `2fe4dcdc323b92e93f759cc3e373521366b7f691` of the Ironclad repository at `[email protected]:microsoft/Ironclad.git`. | ||
| * From the `ironfleet` directory in that repository, run `scons | ||
| --dafny-path=<path>` where `<path>` is the path to the directory | ||
| containing the Dafny 3.4.0 executable. | ||
| * Build the Verus version of IronSHT. | ||
| * Download the Verus source code from commit `96957b633471e4d5a6bc267f9bf0e31555e888db` | ||
| of the repo at `[email protected]:secure-foundations/verus.git`. | ||
| * Build the Verus source code as the repo describes, making sure to use | ||
| `--release` on the `vargo build`. | ||
| * Download the Verus version of IronSHT from commit | ||
| `ea501b56ef92290329ba434fb8b675a5f467de65` of the Verus systems code | ||
| repository at `[email protected]:verus-lang/verus-systems-code.git`. | ||
| * Make a small local update to that repository to make it operate on | ||
| Windows, as follows: In the file | ||
| `ironfleet-comparison/ironsht/csharp/IronSHTClient/Client.cs`, change | ||
| all references to `../liblib.so` to `lib.dll`. | ||
| * From the `ironfleet-comparison` directory, run `scons | ||
| --verus-path=<path>` where `<path>` is the path to the root directory | ||
| for the Verus repository. | ||
| * Copy the resulting `lib.dll` from the `ironfleet-comparison` directory | ||
| to the directory containing this `README.md` (`sys/eval/ironsht`). | ||
| * Prepare to run the experiment. | ||
| * Change directory to the directory containing this `README.md` | ||
| (`sys/eval/ironsht`). | ||
| * Generate certificates with `dotnet <path>/ironsht/bin/CreateIronServiceCerts.dll | ||
| outputdir=certs name=MySHT type=IronSHT addr1=127.0.0.1 port1=4001 | ||
| addr2=127.0.0.1 port2=4002 addr3=127.0.0.1 port3=4003` where `<path>` is | ||
| the path to either the Dafny or Verus IronSHT code. | ||
| * With `pip`, install `numpy` and `scipy`. | ||
| * Update the hardcoded paths `VERUS_PATH` and `DAFNY_PATH` in the script | ||
| `compare.py` to match where those directories are on your machine. | ||
| * Prepare your machine for the experiment by telling Windows to never | ||
| sleep, by telling it to use the "best performance" power mode (to | ||
| disable SpeedStep), and by plugging it into a real charging outlet (not | ||
| just a USB-C connector to a monitor). | ||
| * Run the experiment by running `python compare.py` from this directory. This will | ||
| overwrite the file `raw-data.txt` with its output. | ||
| * Generate the graph by running `python gengraph.py > ..\..\paper\ironfleet-port-plot.tex`. | ||
| This uses the data stored in `raw-data.txt`. | ||
|
|
||
| ### Set 3: node replication performance comparison — Figure 10. | ||
|
|
||
| Set 3 used a Linux Intel-based x86_64 4-CPU NUMA system with 24 cores per CPU. However, a smaller Linux Intel-based x86_64 NUMA system with at least 2 CPUs should reproduce a similar performance pattern. We recommend CloudLab r650. | ||
|
|
@@ -127,3 +80,60 @@ scp '<username>@<node>.cloudlab.us:/mydata/verus-sosp24-artifact/macro-stats/res | |
| scp '<username>@<node>.cloudlab.us:/mydata/verus-sosp24-artifact/macro-stats/results/macro-table.pdf' . | ||
| ``` | ||
|
|
||
| ## Set 2 | ||
|
|
||
| ### Claims | ||
|
|
||
| **TODO.** | ||
|
|
||
| ### Instructions | ||
|
|
||
| **TODO. Code from https://github.com/verus-lang/verified-ironkv?** | ||
|
|
||
| To run this experiment, take the following steps: | ||
|
|
||
| * Build the IronFleet version of IronSHT. | ||
| * Install `dotnet`. | ||
| * Install `scons` with `pip install scons`. | ||
| * Download the Dafny 3.4.0 release, including its executable, from | ||
| `https://github.com/dafny-lang/dafny/releases/download/v3.4.0/dafny-3.4.0-x64-win.zip`. | ||
| * Sync to commit `2fe4dcdc323b92e93f759cc3e373521366b7f691` of the Ironclad repository at `[email protected]:microsoft/Ironclad.git`. | ||
| * From the `ironfleet` directory in that repository, run `scons | ||
| --dafny-path=<path>` where `<path>` is the path to the directory | ||
| containing the Dafny 3.4.0 executable. | ||
| * Build the Verus version of IronSHT. | ||
| * Download the Verus source code from commit `96957b633471e4d5a6bc267f9bf0e31555e888db` | ||
| of the repo at `[email protected]:secure-foundations/verus.git`. | ||
| * Build the Verus source code as the repo describes, making sure to use | ||
| `--release` on the `vargo build`. | ||
| * Download the Verus version of IronSHT from commit | ||
| `ea501b56ef92290329ba434fb8b675a5f467de65` of the Verus systems code | ||
| repository at `[email protected]:verus-lang/verus-systems-code.git`. | ||
| * Make a small local update to that repository to make it operate on | ||
| Windows, as follows: In the file | ||
| `ironfleet-comparison/ironsht/csharp/IronSHTClient/Client.cs`, change | ||
| all references to `../liblib.so` to `lib.dll`. | ||
| * From the `ironfleet-comparison` directory, run `scons | ||
| --verus-path=<path>` where `<path>` is the path to the root directory | ||
| for the Verus repository. | ||
| * Copy the resulting `lib.dll` from the `ironfleet-comparison` directory | ||
| to the directory containing this `README.md` (`sys/eval/ironsht`). | ||
| * Prepare to run the experiment. | ||
| * Change directory to the directory containing this `README.md` | ||
| (`sys/eval/ironsht`). | ||
| * Generate certificates with `dotnet <path>/ironsht/bin/CreateIronServiceCerts.dll | ||
| outputdir=certs name=MySHT type=IronSHT addr1=127.0.0.1 port1=4001 | ||
| addr2=127.0.0.1 port2=4002 addr3=127.0.0.1 port3=4003` where `<path>` is | ||
| the path to either the Dafny or Verus IronSHT code. | ||
| * With `pip`, install `numpy` and `scipy`. | ||
| * Update the hardcoded paths `VERUS_PATH` and `DAFNY_PATH` in the script | ||
| `compare.py` to match where those directories are on your machine. | ||
| * Prepare your machine for the experiment by telling Windows to never | ||
| sleep, by telling it to use the "best performance" power mode (to | ||
| disable SpeedStep), and by plugging it into a real charging outlet (not | ||
| just a USB-C connector to a monitor). | ||
| * Run the experiment by running `python compare.py` from this directory. This will | ||
| overwrite the file `raw-data.txt` with its output. | ||
| * Generate the graph by running `python gengraph.py > ..\..\paper\ironfleet-port-plot.tex`. | ||
| This uses the data stored in `raw-data.txt`. | ||
|
|
||