search

tamarin-prover / tamarin-prover

Main source code repository of the Tamarin prover for security protocol verification.
https://tamarin-prover.com/
GNU General Public License v3.0
408 stars 131 forks source link

Performance regression in diff models in Tamarin 180 vs 161 #615

Open swesemeyer opened 7 months ago

swesemeyer commented 7 months ago

Hi,

I have a diff model which runs within 2 minutes on my multi-core machine as it can use all 32 cores when I use Tamarin-161

However, running the same model using Tamarin-180, it seems to be restricted to using at most 2 cores resulting in a massive slowdown.

Has anyone else noticed this?

swesemeyer commented 7 months ago

time tamarin-prover-180 model.spthy --diff --prove && date

yields:

processing time: 2897.92s

RHS : executability_A1_A2 (exists-trace): verified (3 steps) LHS : executability_A1_A2 (exists-trace): verified (3 steps) RHS : executability_A1_A3 (exists-trace): verified (3 steps) LHS : executability_A1_A3 (exists-trace): verified (3 steps) RHS : executability_A1_A4 (exists-trace): verified (3 steps) LHS : executability_A1_A4 (exists-trace): verified (3 steps) RHS : executability_success (exists-trace): verified (5 steps) LHS : executability_success (exists-trace): verified (5 steps) RHS : executability_failure (exists-trace): verified (5 steps) LHS : executability_failure (exists-trace): verified (5 steps) DiffLemma: Observational_equivalence : verified (899 steps)

==============================================================================

real 48m18.071s user 70m38.063s sys 5m9.406s Fri 2 Feb 17:33:19 GMT 2024

while time tamarin-prover-161 model.spthy --diff --prove && date yields RHS : executability_A1_A2 (exists-trace): verified (3 steps) LHS : executability_A1_A2 (exists-trace): verified (3 steps) RHS : executability_A1_A3 (exists-trace): verified (3 steps) LHS : executability_A1_A3 (exists-trace): verified (3 steps) RHS : executability_A1_A4 (exists-trace): verified (3 steps) LHS : executability_A1_A4 (exists-trace): verified (3 steps) RHS : executability_success (exists-trace): verified (5 steps) LHS : executability_success (exists-trace): verified (5 steps) RHS : executability_failure (exists-trace): verified (5 steps) LHS : executability_failure (exists-trace): verified (5 steps) DiffLemma: Observational_equivalence : verified (899 steps)

==============================================================================

real 1m3.381s user 15m10.156s sys 11m15.469s Fri 2 Feb 18:54:09 GMT 2024

swesemeyer commented 7 months ago

regression.spthy.zip

Please find attached a file that includes the model that exhibits the above behaviour.

Hopefully that will help troubleshoot the issue.

swesemeyer commented 7 months ago

tamarin-prover-180 --version tamarin-prover 1.8.0, (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, 2010-2023

This program comes with ABSOLUTELY NO WARRANTY. It is free software, and you are welcome to redistribute it according to its LICENSE, see 'https://github.com/tamarin-prover/tamarin-prover/blob/master/LICENSE'.

maude tool: 'maude' checking version: 3.1. OK. checking installation: OK. Generated from: Tamarin version 1.8.0 Maude version 3.1 Git revision: f172d7f00b1485446a1e7a42dc14623c2189cc42, branch: master Compiled at: 2023-11-11 13:11:25.424495998 UTC

rsasse commented 6 months ago

Sorry for not responding quicker, but I have no idea what triggers this concretely. This is very unfortunate. Also, looking at the number it is not only a lack of parallelization, but some steps do seem to take longer, as it's 75 minutes (user+sys) vs 26 minutes.

No idea if that's a Tamarin internal issue, a Haskell version issue (different behavior of the runtime), or something else, so this will not be easy to debug.

swesemeyer commented 6 months ago

Hi Ralf,

The server I run this on has the same environment for both, the only difference is the tamarin binary. (Ubuntu 22.04) The slowdown also happens on my laptop which is an up-to-date Fedora 39 install. Does my test file not exhibit that behaviour in your environment? Let me know if you need any further info.

Cheers, Steve

From: Ralf Sasse @.> Sent: 12 March 2024 14:43 To: tamarin-prover/tamarin-prover @.> Cc: Wesemeyer, Steve Dr (Comp Sci & Elec Eng) @.>; Author @.> Subject: Re: [tamarin-prover/tamarin-prover] Performance regression in diff models in Tamarin 180 vs 161 (Issue #615)

Sorry for not responding quicker, but I have no idea what triggers this concretely. This is very unfortunate. Also, looking at the number it is not only a lack of parallelization, but some steps do seem to take longer, as it's 75 minutes (user+sys) vs 26 minutes.

No idea if that's a Tamarin internal issue, a Haskell version issue (different behavior of the runtime), or something else, so this will not be easy to debug.

— Reply to this email directly, view it on GitHubhttps://github.com/tamarin-prover/tamarin-prover/issues/615#issuecomment-1991815131, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABR34ZYWUV4VUFR5GAGD7X3YX4IADAVCNFSM6AAAAABCW7H4UOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSOJRHAYTKMJTGE. You are receiving this because you authored the thread.

rsasse commented 6 months ago

Hi Steve,

Sorry if that was not clear. The change of GHC+runtime is simply due to the different version of Tamarin being compiled with different GHC versions. There is nothing on your end to check or change.

Cheers, Ralf

swesemeyer commented 4 months ago

Just to add that this does not seem to be confined to just diff models. I have noticed in my normal models that Tamarin only uses 2 or 3 cores for some goals (in interactive mode) while using all cores for others. Running the same model in Tamarin 1.6.1 shows that it can make us of all cores when solving the same goal.

As a result, most of my models take less time to prove in 1.6.1 than in 1.8.0.