Performance regression in diff models in Tamarin 180 vs 161 #615
Comments
|
time tamarin-prover-180 model.spthy --diff --prove && date yields: processing time: 2897.92s RHS : executability_A1_A2 (exists-trace): verified (3 steps) ============================================================================== real 48m18.071s while ============================================================================== real 1m3.381s |
|
Please find attached a file that includes the model that exhibits the above behaviour. Hopefully that will help troubleshoot the issue. |
|
tamarin-prover-180 --version This program comes with ABSOLUTELY NO WARRANTY. It is free software, and you maude tool: 'maude' |
|
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. |
|
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 GitHub<#615 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABR34ZYWUV4VUFR5GAGD7X3YX4IADAVCNFSM6AAAAABCW7H4UOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSOJRHAYTKMJTGE>.
You are receiving this because you authored the thread.
|
|
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, |
|
Just to add that this does not seem to be confined to just diff models. As a result, most of my models take less time to prove in 1.6.1 than in 1.8.0. |
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?
The text was updated successfully, but these errors were encountered: