From d91b91a6350d0e083f467079d3fd5171624092bc Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 19 Aug 2024 17:35:12 +0200 Subject: [PATCH] Move IronKV instructions, add TODO --- site/guide.md | 104 +++++++++++++++++++++++++++----------------------- 1 file changed, 57 insertions(+), 47 deletions(-) diff --git a/site/guide.md b/site/guide.md index 4cdb38d..b3ab162 100644 --- a/site/guide.md +++ b/site/guide.md @@ -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 `git@github.com:microsoft/Ironclad.git`. - * From the `ironfleet` directory in that repository, run `scons - --dafny-path=` where `` 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 `git@github.com: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 `git@github.com: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=` where `` 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 /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 `` 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 '@.cloudlab.us:/mydata/verus-sosp24-artifact/macro-stats/res scp '@.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 `git@github.com:microsoft/Ironclad.git`. + * From the `ironfleet` directory in that repository, run `scons + --dafny-path=` where `` 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 `git@github.com: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 `git@github.com: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=` where `` 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 /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 `` 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`. +