Verifying many file

[seebees]

Dafny version

4.x

Code to produce this issue

https://github.com/aws/aws-cryptographic-material-providers-library-dafny/blob/554ee57be21444c28658fb9adbcd6b91a635743c/SharedMakefileV2.mk#L68-L78

    dafny \
        -vcsCores:$(CORES) \
        -compile:0 \
        -definiteAssignment:3 \
        -quantifierSyntax:3 \
        -unicodeChar:0 \
        -functionSyntax:3 \
        -verificationLogger:csv \
        -timeLimit:100 \
        -trace \
        `find . -name *.dfy`

Command to run and resulting output

We used to verify many files at once and use the cores option to parallelize. However this only controls how many Z3 processes are spawned.

For large projects even with fast verification this takes much longer than expected.

For example: https://github.com/aws/aws-cryptographic-material-providers-library-dafny/actions/runs/6487004883/job/17616386544

See: push-ci-verification / verification (AwsCryptographicMaterialProviders, macos-latest) succeeded yesterday in 46m 37s

Running abstract interpretation...
[TRACE] Using prover: /Users/runner/hostedtoolcache/dafny/4.2.0/x64/z3/bin/z3-4.12.1

Running abstract interpretation...
  [0.781471 s]
  [3.319017 s]
  [3.121533 s]
Linearising   [0.633863 s]
Linearising   [42.031375 s]
Linearising   [42.390211 s]
Linearising   [42.200783 s]
Linearising   [42.725311 s]
Linearising   [2.392666 s]
Linearising   [2.664374 s]
Linearising   [2.599615 s]
Linearising   [1.445773 s]
Linearising   [0.959644 s]
Linearising   [1.634828 s]
Linearising   [2.492221 s]
Linearising   [3.234185 s]

Running abstract interpretation...
Linearising   [3.388255 s]
Linearising   [1.32112 s]
Linearising   [0.654406 s]
Linearising   [1.126669 s]
Linearising   [9.129714 s]
Linearising   [0.913611 s]
Linearising   [2.331469 s]
Linearising   [2.374349 s]
Linearising   [1.150231 s]
Linearising   [1.916181 s]
Linearising   [1.454213 s]
Coalescing blocks...
Linearising   [2.312987 s]
Linearising   [2.705753 s]
Inlining...
  [14.163282 s]
  [68.547 s, solver resource count: 140873, 27 proof obligations]  verified

What happened?

My guess is that the Dafny process that is feeding the Z3 processes has some major optimization opportunities. First my guess is that controlling the number of files being inlined and linearized will help.

But my guess is that the larger optimization has to do with how Dafny process some source to send it to Z3. If you flip the way you handle this so that instead of trying to verify all the files at once you verify a single file at a time, you get much better performance in the aggregate.

Our project basically include all the Dafny, so if you verify one file or all the files the same amount of Dafny is loaded. And yet with the overhead of all that running a process per file is much faster once you have a few cores available.

I suspect that the process of cleaning up and sorting "stuff" before building the boogie operates on all files to verify. Even though only a small subset of that is sent to Z3. This is why sending lots of files to verify results in so much overhead.

Our current verification target now looks like this https://github.com/aws/aws-cryptographic-material-providers-library-dafny/blob/main/SharedMakefileV2.mk#L81

# Proof of correctness for the math below
#  function Z3_PROCESSES(cpus:nat): nat
#  { if cpus >= 3 then 2 else 1 }

#  function DAFNY_PROCESSES(cpus: nat): nat
#   requires 0 < cpus // 0 cpus would do no work!
#  { (cpus - 1 )/Z3_PROCESSES(cpus) }

#  lemma Correct(cpus:nat)
#    ensures DAFNY_PROCESSES(cpus) * Z3_PROCESSES(cpus) <= cpus
#  {}

# Verify the entire project
verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
verify:DAFNY_PROCESSES=$(shell echo $$(( ($(CORES) - 1 ) / ($(CORES) >= 3 ? 2 : 1))))
verify:
    find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny \
        -vcsCores:$(Z3_PROCESSES) \
        -compile:0 \
        -definiteAssignment:3 \
        -quantifierSyntax:3 \
        -unicodeChar:0 \
        -functionSyntax:3 \
        -verificationLogger:csv \
        -timeLimit:100 \
        -trace \
        %

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

I would like to debug this, but on the most recent Dafny version. Once your project updates to the latest Dafny version, please ping this issue so we can look at it again.