-
Notifications
You must be signed in to change notification settings - Fork 122
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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: