search

microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

dafny version #3

Closed jyizheng closed 4 years ago

jyizheng commented 4 years ago

Hi,

Which version of dafny should be used for the current code? I have downloaded dafny 2.3.0 and add the *.dll to VS2017. I got errors below when building the code.

Severity Code Description Project File Line Suppression State Error Application Configuration file "app.config" is invalid. Could not find file 'C:\Users\andyj\Armada-master\Source\ArmadaDriver\app.config'. Armada C:\Users\andyj\Armada-master\Source\ArmadaDriver\app.config
Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 14327 Active Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 13491 Active Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 7274 Active Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 5791 Active

LukeXuan commented 4 years ago

Which version of dafny should be used for the current code?

For the master branch of Armada, you will need Dafny@d16450. However, your problem doesn't seem to be caused by dafny version.

We didn't make it clear about building instructions in the README file. To build Armada, you will need to build boogie@v2.4.21 first. I'm composing a BUILD.md file to provide detailed instructions. Could you help me verify the following instructions work for you? We also forgot to include one of the config file necessary to build the tool, you will need to pull from the master first before retry.

Building on Linux

This instruction is adapted from the INSTALL.md from dafny repo. BASE-DIRECTORY is assumed to be your base directory for building Armada.

  1. Dependencies: Install Mono from the official repositories; the version in most distribution repositories is too out of date. The mono-devel package is what you need. On Fedora, you'll also need the msbuild package.

  2. Create an empty base directory and download nuget

    mkdir BASE-DIRECTORY cd BASE-DIRECTORY wget https://nuget.org/nuget.exe

  3. Download and build Boogie:

    git clone --branch v2.4.21 https://github.com/boogie-org/boogie cd boogie mono ../nuget.exe restore Source/Boogie.sln msbuild Source/Boogie.sln cd ..

  4. Download and build Armada:

    cd BASE-DIRECTORY git clone https://github.com/microsoft/armada mono ../nuget.exe restore armada/Source/Armada.sln msbuild armada/Source/Armada.sln

  5. An executable named Armada.exe should be built in directory armada/Binaries/. You will also need scons, Dafny@d16450, and Z3@4.8.4 to run the tests.

Using the Artifact Package

Our PLDI'20 paper is published with an artifact package. It is a self-contained package with all dependencies installed. You can find the package as well as instructions here.

jyizheng commented 4 years ago

Thanks for the instructions. I have tried them. It works. I can build Armada.exe now. Only two minor issues in step 1 and 3.

In step 1, wget https://nuget.org/nuget.exe downloads nuget.exe with version 2.8.6 on my machine. I got an error below when compiling boogie.

The 'NUnit 3.12.0' package requires NuGet client version '2.12' or above, but the current NuGet version is '2.8.60717.93'.

I fixed it by manually downloading nuget.exe v3.3.0.

In step 3, for mono ../nuget.exe restore armada/Source/Armada.sln, need to change ../nuget.exe to ./nuget.exe

jyizheng commented 4 years ago

I also generated and tested the proofs following steps here: https://github.com/microsoft/Armada#generating-and-testing-proofs

I got the results below. There is one proof that got a timeout. Does it matter?

Running abstract interpretation... [0.07198 s] [TRACE] Using prover: /home/andy/code/Armada/dafny/Binaries/z3/bin/z3

Verifying CheckWellformed$$Math__modautoi.default.eq__mod ... [0.620 s, 1 proof obligation] verified

Verifying CheckWellformed$$Math__modautoi.default.ModAuto ... [0.144 s, 15 proof obligations] verified

Verifying CheckWellformed$$Math__modautoi.default.modautopred1 ... [0.115 s, 4 proof obligations] verified

Verifying CheckWellformed$$Math__modautoi.default.modautopred2 ... [0.104 s, 4 proof obligations] verified

Verifying CheckWellformed$$Math__modautoi.default.lemmamodauto ... [0.109 s, 1 proof obligation] verified

Verifying Impl$$Math__modautoi.default.lemmamodauto ... [296.963 s, 80 proof obligations] timed out mod_auto.i.dfy(45,6): Verification of 'Impl$$Math__modautoi.default.lemmamodauto' timed out after 240 seconds

Verifying CheckWellformed$$Math__modautoi.default.lemmamodauto__induction ... [1.442 s, 8 proof obligations] verified

Verifying Impl$$Math__modautoi.default.lemmamodauto__induction ... [0.327 s, 25 proof obligations] verified

Verifying CheckWellformed$$Math__modautoi.default.lemmamodautoinductionforall ... [0.122 s, 8 proof obligations] verified

Verifying Impl$$Math__modautoi.default.lemmamodautoinductionforall ... [0.246 s, 23 proof obligations] verified

Dafny program verifier finished with 9 verified, 0 errors, 1 time out

LukeXuan commented 4 years ago

Yes, time outs do matter. Only if all the proof obligations are verified, instead of error or timed out, the Armada program is verified correct.

I'm pretty sure the scons scripts can verify without time out on our machines. However, the following factors can affect the verification time:

jyizheng commented 4 years ago

Before I try to change -j arugment for scons, I first double-checked the version of z3 and dafny on my machine. For dafny, git log shows I am using the right version (commit d164508). For z3, I downloaded the prebuilt release (z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04.zip) for z3 website. It should be just right. However, I noticed that under dafny folder, there is a sub-folder with name z3 and a binary with name z3.exe. The binary (z3.exe) was generated when I was building dafny's source code. The subfold was created when I copied the prebuilt z3 release to dafny by following the steps from website (https://github.com/dafny-lang/dafny/blob/master/INSTALL.md). I am wondering which z3 will be used in this case? Do I need to make sure dafny/Binaries/z3.exe and dafny/Binaries/z3/bin/z3 to be the same?

LukeXuan commented 4 years ago

I think dafny/Binaries/z3/bin/z3 is the binary used for dafny, at least it is the case on Linux.

jyizheng commented 4 years ago

Thanks for the clarification. I also tuned the -j argument from 4 to 2 for command scons -j <n> -f SConstruct2 --DAFNYPATH=<dafny-path> . As stated previously, I got a timeout for -j 4. For -j 2, I got the error below:

scons: *** [Test/mcslock/L4_L5/convert.vdfy] Source Test/mcslock/L4_L5_helper.dfy' not found, needed by targetTest/mcslock/L4_L5/convert.vdfy'.

I also did a search in the source code directory. I didn't find this file.

LukeXuan commented 4 years ago

You are right. Two helper files were missing in the repository. I forgot to git add -f them when we made our code open source. I have just pushed a commit to restore those two files. Please pull again and it should verify now.

jyizheng commented 4 years ago

Thanks a lot. All code got verified on my machine too with the latest code.