-
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.
Import macrobenchmark statistics evaluation automation
Co-authored-by: Andrea Lattuada <[email protected]> Co-authored-by: Jay Lorch <[email protected]> Co-authored-by: Jon Howell <[email protected]> Co-authored-by: Hayley LeBlanc <[email protected]> Co-authored-by: Travis Hance <[email protected]>
- Loading branch information
6 people
committed
Aug 15, 2024
1 parent
bb7be20
commit cdfd365
Showing
27 changed files
with
1,513 additions
and
0 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 |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| /repos/ | ||
| /results/ |
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 |
|---|---|---|
| @@ -0,0 +1,5 @@ | ||
|
|
||
| Install docker, run `bash run.sh`. | ||
|
|
||
| Produces results in `results/`, in particular `results.json`, `results-latex-commands.tex`, `results-latex-table.tex`. | ||
|
|
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 |
|---|---|---|
| @@ -0,0 +1,66 @@ | ||
| #! /bin/bash | ||
|
|
||
| # unzip libicu-dev libgomp1 python3 | ||
|
|
||
| DAFNY_THREADS=8 | ||
|
|
||
| VERIFY_IRONSHT=1 | ||
|
|
||
| set -e | ||
| set -x | ||
|
|
||
| . lib.sh | ||
|
|
||
| if [ $# -lt 1 ]; then | ||
| echo "usage: $0 <command>" | ||
| exit 1 | ||
| fi | ||
|
|
||
| RESULTS_DIR=$1 | ||
|
|
||
| print_header "setting up repos/" | ||
|
|
||
| if [ ! -d "repos" ]; then | ||
| mkdir repos | ||
| fi | ||
|
|
||
| print_header "cloning or updating repositories" | ||
|
|
||
| clone_and_update_repository "ironclad" "main" "https://github.com/microsoft/Ironclad.git" | ||
|
|
||
| (cd repos; | ||
| if [ ! -d "dafny-3.4.0" ]; then | ||
| mkdir dafny-3.4.0 | ||
| cd dafny-3.4.0 | ||
| curl -LO https://github.com/dafny-lang/dafny/releases/download/v3.4.0/dafny-3.4.0-x64-ubuntu-16.04.zip | ||
| unzip dafny-3.4.0-x64-ubuntu-16.04.zip | ||
| rm dafny-3.4.0-x64-ubuntu-16.04.zip | ||
| fi) | ||
|
|
||
| print_header "verifying" | ||
|
|
||
| cd $RESULTS_DIR | ||
|
|
||
| echo $DAFNY_THREADS > dafny-num-threads.txt | ||
|
|
||
| if [ $VERIFY_IRONSHT -eq 1 ]; then | ||
| print_step "verifying ironsht" | ||
|
|
||
| mkdir -p ironsht && cd ironsht | ||
|
|
||
| DAFNY_EXE=../../repos/dafny-3.4.0/dafny/dafny | ||
|
|
||
| IRONSHT_FILES=$(sed -e 's/^/..\/..\/repos\/ironclad\//' ../../ironsht_files.txt | tr '\n' ' ' | tr -d '\r') | ||
| IRONSHT_NONLINEAR_FILES=$(sed -e 's/^/..\/..\/repos\/ironclad\//' ../../ironsht_files_nonlinear.txt | tr '\n' ' ' | tr -d '\r') | ||
|
|
||
| python3 ../../time.py dafny-verification-parallel.output.txt dafny-verification-parallel.time.txt \ | ||
| $DAFNY_EXE /compile:0 /arith:5 /noCheating:1 /trace /vcsCores:$DAFNY_THREADS $IRONSHT_FILES | ||
| python3 ../../time.py dafny-verification-parallel-nonlinear.output.txt dafny-verification-parallel-nonlinear.time.txt \ | ||
| $DAFNY_EXE /compile:0 /arith:2 /noCheating:1 /trace /vcsCores:$DAFNY_THREADS $IRONSHT_NONLINEAR_FILES | ||
| python3 ../../time.py dafny-verification-singlethread.output.txt dafny-verification-singlethread.time.txt \ | ||
| $DAFNY_EXE /compile:0 /arith:5 /noCheating:1 /trace /vcsCores:1 $IRONSHT_FILES | ||
| python3 ../../time.py dafny-verification-singlethread-nonlinear.output.txt dafny-verification-singlethread-nonlinear.time.txt \ | ||
| $DAFNY_EXE /compile:0 /arith:2 /noCheating:1 /trace /vcsCores:1 $IRONSHT_NONLINEAR_FILES | ||
|
|
||
| cd .. | ||
| fi |
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 |
|---|---|---|
| @@ -0,0 +1,48 @@ | ||
| ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.s.dfy | ||
| ironfleet/src/Dafny/Distributed/Common/Framework/Environment.s.dfy | ||
| ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy | ||
| ironfleet/src/Dafny/Distributed/Common/Native/Io.s.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mod_auto.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mod_auto_proofs.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mul.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mul_auto.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mul_auto_proofs.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../Common/Collections/Seqs.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../Common/CmdLineParser.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../Common/NetClient.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/CmdLineParser.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/Host.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/NetSHT.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/SchedulerImpl.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/SchedulerModel.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/Unsendable.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/../../Common/Logic/Option.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/../../Common/Native/NativeTypes.s.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/../Common/GenericMarshalling.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/../Common/GenericRefinement.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/../Common/NodeIdentity.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/AppInterface.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/AppInterfaceConcrete.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/CMessage.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/ConstantsState.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/DelegationLookup.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/Delegations.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/HostModel.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/HostState.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/PacketParsing.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/Parameters.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/SHTConcreteConfiguration.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/SingleDeliveryModel.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/SHT/SingleDeliveryState.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/Scheduler.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Configuration.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Delegations.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Host.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Keys.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Message.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Network.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/Parameters.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/SingleDelivery.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Protocol/SHT/SingleMessage.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Services/SHT/Main.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy |
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 |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/mul_nonlinear.i.dfy | ||
| ironfleet/src/Dafny/Distributed/Impl/LiveSHT/../../../Libraries/Math/div_nonlinear.i.dfy |
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 |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
|
|
||
| print_header() { | ||
| local message=$1 | ||
| echo -e "\033[32m■ $message\033[0m" | ||
| } | ||
|
|
||
| print_step() { | ||
| local message=$1 | ||
| echo -e "\033[34m ■ $message\033[0m" | ||
| } | ||
|
|
||
| clone_and_update_repository() { | ||
| print_step "cloning or updating $1" | ||
|
|
||
| cd repos | ||
|
|
||
| local repo_name=$1 | ||
| local branch=$2 | ||
| local repo_url=$3 | ||
| local repo_path="$repo_name" | ||
|
|
||
| if [ ! -d "$repo_path" ]; then | ||
| GIT_SSH_COMMAND="ssh -o StrictHostKeyChecking=no -o UserKnownHostsFile=/dev/null" \ | ||
| git clone -b $branch --single-branch --depth 1 $repo_url $repo_path | ||
| fi | ||
| (cd $repo_path; | ||
| GIT_SSH_COMMAND="ssh -o StrictHostKeyChecking=no -o UserKnownHostsFile=/dev/null" \ | ||
| git pull --ff-only) | ||
|
|
||
| cd .. # repos | ||
| } | ||
|
|
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 |
|---|---|---|
| @@ -0,0 +1,26 @@ | ||
| #! /bin/bash | ||
|
|
||
| DAFNY_THREADS=8 | ||
|
|
||
| set -e | ||
| set -x | ||
|
|
||
| . lib.sh | ||
|
|
||
| if [ $# -lt 1 ]; then | ||
| echo "usage: $0 <command>" | ||
| exit 1 | ||
| fi | ||
|
|
||
| RESULTS_DIR=$1 | ||
|
|
||
| print_header "setting up repos/" | ||
|
|
||
| if [ ! -d "repos" ]; then | ||
| mkdir repos | ||
| fi | ||
|
|
||
| print_header "cloning or updating repositories" | ||
|
|
||
| clone_and_update_repository "ironsync" "osdi2023-artifact" "[email protected]:secure-foundations/ironsync-osdi2023.git" | ||
|
|
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 |
|---|---|---|
| @@ -0,0 +1,65 @@ | ||
| total 4407904 | ||
| -rw-r--r-- 1 andreal1 staff 57297145 Dec 4 14:27 log-2023-12-04T13.27.28.5706360+00.00-concurrency-node-replication-Interface.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2059208 Dec 4 14:27 log-2023-12-04T13.27.48.8646435+00.00-concurrency-node-replication-Interface.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 953440 Dec 4 14:27 log-2023-12-04T13.27.52.8481608+00.00-concurrency-node-replication-NRSpec.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 1569107 Dec 4 14:27 log-2023-12-04T13.27.56.0336421+00.00-concurrency-framework-StateMachines.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 1633504 Dec 4 14:28 log-2023-12-04T13.27.56.0336421+00.00-concurrency-framework-StateMachines.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 1318875 Dec 4 14:28 log-2023-12-04T13.27.56.0336421+00.00-concurrency-framework-StateMachines.s.dfy.smt2.2 | ||
| -rw-r--r-- 1 andreal1 staff 462611 Dec 4 14:28 log-2023-12-04T13.28.01.1769232+00.00-concurrency-node-replication-Linearize.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 669652 Dec 4 14:28 log-2023-12-04T13.28.01.1769232+00.00-concurrency-node-replication-Linearize.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 1204608 Dec 4 14:28 log-2023-12-04T13.28.05.1551617+00.00-concurrency-framework-AsyncSSM.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 1943380 Dec 4 14:28 log-2023-12-04T13.28.05.1551617+00.00-concurrency-framework-AsyncSSM.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 9996892 Dec 4 14:28 log-2023-12-04T13.28.05.1551617+00.00-concurrency-framework-AsyncSSM.s.dfy.smt2.2 | ||
| -rw-r--r-- 1 andreal1 staff 449020 Dec 4 14:28 log-2023-12-04T13.28.12.0310287+00.00-concurrency-framework-PCM.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2916518 Dec 4 14:28 log-2023-12-04T13.28.12.0310287+00.00-concurrency-framework-PCM.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 10774017 Dec 4 14:28 log-2023-12-04T13.28.16.2144152+00.00-lib-Lang-LinearSequence.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 5760789 Dec 4 14:28 log-2023-12-04T13.28.21.4328978+00.00-lib-Lang-NativeTypes.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2269925 Dec 4 14:28 log-2023-12-04T13.28.25.8366585+00.00-lib-Lang-LinearMaybe.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 77624752 Dec 4 14:28 log-2023-12-04T13.28.29.4444561+00.00-concurrency-node-replication-Init.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 3943038 Dec 4 14:29 log-2023-12-04T13.28.55.6496438+00.00-concurrency-node-replication-Impl.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 203887529 Dec 4 14:29 log-2023-12-04T13.28.55.6496438+00.00-concurrency-node-replication-Impl.i.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 177498943 Dec 4 14:32 log-2023-12-04T13.29.46.8144611+00.00-concurrency-node-replication-InfiniteLogTokens.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 303962692 Dec 4 14:34 log-2023-12-04T13.32.17.3468999+00.00-concurrency-node-replication-InfiniteLog.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 10332790 Dec 4 14:34 log-2023-12-04T13.34.49.4593714+00.00-concurrency-framework-AsyncSSM.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 715368 Dec 4 14:34 log-2023-12-04T13.34.54.8048547+00.00-lib-Base-Option.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2464250 Dec 4 14:35 log-2023-12-04T13.34.57.7347808+00.00-concurrency-node-replication-Constants.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 671304 Dec 4 14:35 log-2023-12-04T13.35.01.0773862+00.00-concurrency-framework-GlinearMap.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 6803557 Dec 4 14:35 log-2023-12-04T13.35.03.8988362+00.00-concurrency-framework-Ptrs.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 719446 Dec 4 14:35 log-2023-12-04T13.35.08.2318001+00.00-concurrency-framework-GlinearOption.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 49393561 Dec 4 14:35 log-2023-12-04T13.35.11.4975346+00.00-lib-Lang-LinearSequence.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 25209698 Dec 4 14:35 log-2023-12-04T13.35.23.7867456+00.00-concurrency-node-replication-rwlock-Impl.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2512752 Dec 4 14:35 log-2023-12-04T13.35.33.3077550+00.00-concurrency-framework-Atomic.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2644872 Dec 4 14:35 log-2023-12-04T13.35.33.3077550+00.00-concurrency-framework-Atomic.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 714994 Dec 4 14:35 log-2023-12-04T13.35.37.8969898+00.00-concurrency-framework-Cells.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 348351 Dec 4 14:35 log-2023-12-04T13.35.40.8770008+00.00-concurrency-node-replication-Runtime.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 36868986 Dec 4 14:35 log-2023-12-04T13.35.45.5833056+00.00-concurrency-node-replication-rwlock-RwLock.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 33457375 Dec 4 14:36 log-2023-12-04T13.35.45.5833056+00.00-concurrency-node-replication-rwlock-RwLock.i.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 3258600 Dec 4 14:36 log-2023-12-04T13.36.05.7455203+00.00-concurrency-framework-Rw.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 3437851 Dec 4 14:36 log-2023-12-04T13.36.05.7455203+00.00-concurrency-framework-Rw.i.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 9118089 Dec 4 14:36 log-2023-12-04T13.36.05.7455203+00.00-concurrency-framework-Rw.i.dfy.smt2.2 | ||
| -rw-r--r-- 1 andreal1 staff 21598593 Dec 4 14:36 log-2023-12-04T13.36.05.7455203+00.00-concurrency-framework-Rw.i.dfy.smt2.3 | ||
| -rw-r--r-- 1 andreal1 staff 512073 Dec 4 14:36 log-2023-12-04T13.36.16.9074371+00.00-concurrency-framework-PCMExt.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2355472 Dec 4 14:36 log-2023-12-04T13.36.16.9074371+00.00-concurrency-framework-PCMExt.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 4421271 Dec 4 14:36 log-2023-12-04T13.36.21.0021382+00.00-concurrency-framework-PCMWrap.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2045677 Dec 4 14:36 log-2023-12-04T13.36.21.0021382+00.00-concurrency-framework-PCMWrap.s.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 9751665 Dec 4 14:36 log-2023-12-04T13.36.25.8294379+00.00-concurrency-scache-rwlock-FullMap.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 2450644 Dec 4 14:36 log-2023-12-04T13.36.30.9493731+00.00-concurrency-scache-rwlock-MapSum.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 4241652 Dec 4 14:36 log-2023-12-04T13.36.36.9273297+00.00-concurrency-scache-ClientCounter.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 7604270 Dec 4 14:36 log-2023-12-04T13.36.36.9273297+00.00-concurrency-scache-ClientCounter.i.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 1372031 Dec 4 14:36 log-2023-12-04T13.36.42.5543811+00.00-concurrency-framework-BasicPCM.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 223401764 Dec 4 14:37 log-2023-12-04T13.36.46.1241424+00.00-concurrency-node-replication-CyclicBufferTokens.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 270044583 Dec 4 14:39 log-2023-12-04T13.37.50.9990527+00.00-concurrency-node-replication-CyclicBuffer.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 4348458 Dec 4 14:39 log-2023-12-04T13.39.31.7607858+00.00-concurrency-framework-MultiRw.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 3879802 Dec 4 14:39 log-2023-12-04T13.39.31.7607858+00.00-concurrency-framework-MultiRw.i.dfy.smt2.1 | ||
| -rw-r--r-- 1 andreal1 staff 17266919 Dec 4 14:39 log-2023-12-04T13.39.31.7607858+00.00-concurrency-framework-MultiRw.i.dfy.smt2.2 | ||
| -rw-r--r-- 1 andreal1 staff 37694895 Dec 4 14:39 log-2023-12-04T13.39.31.7607858+00.00-concurrency-framework-MultiRw.i.dfy.smt2.3 | ||
| -rw-r--r-- 1 andreal1 staff 37737165 Dec 4 14:39 log-2023-12-04T13.39.48.0049473+00.00-lib-Base-Multisets.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 21588617 Dec 4 14:40 log-2023-12-04T13.39.59.3772034+00.00-lib-Base-Maps.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 343879 Dec 4 14:40 log-2023-12-04T13.40.06.4714029+00.00-lib-Base-MapRemove.s.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 92099958 Dec 4 14:40 log-2023-12-04T13.40.09.5477358+00.00-lib-Base-sequences.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 1318589 Dec 4 14:40 log-2023-12-04T13.40.37.4333509+00.00-lib-Base-mathematics.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 60608306 Dec 4 14:40 log-2023-12-04T13.40.41.1967269+00.00-concurrency-node-replication-FlatCombinerTokens.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 55116219 Dec 4 14:41 log-2023-12-04T13.40.57.0237983+00.00-concurrency-node-replication-FlatCombiner.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 167790118 Dec 4 14:43 log-2023-12-04T13.41.56.3070071+00.00-concurrency-node-replication-InfiniteLog_Refines_NRSimple.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 22366777 Dec 4 14:43 log-2023-12-04T13.43.25.2015735+00.00-concurrency-node-replication-NRSimple.i.dfy.smt2 | ||
| -rw-r--r-- 1 andreal1 staff 33915255 Dec 4 14:43 log-2023-12-04T13.43.32.8322910+00.00-concurrency-node-replication-Linearize.i.dfy.smt2 |
Oops, something went wrong.