Counterintuitive Discrepancy in PRISM Runtimes

[Stamina Model Checker]

We ran a few different models on the exact same version of PRISM with the same version of openJDK and openJRE on two different machines: one with a lot better specs than the other. The one with the better specs is an AMD Ryzen Threadripper with 128 GB RAM, and the one with the worse specs is a VM running on a host machine with an i7-8700 CPU and 16 GB RAM. The VM is allocated two to four cores of the CPU.

In both cases, the model building took about the same amount of time, but the model checking was much faster on the VM (which has worse specs) than the original machine (which has better specs)

For this model, we observed:
5m11.580s (311.58 s) on PRISM on Original Machine
3m31.887s (211.887 s) on PRISM on the VM

Versions:

PRISM: v4.5 (git tag)
openjdk 11.0.18 2023-01-17
OpenJDK Runtime Environment (build 11.0.18+10-post-Debian-1deb11u1)
OpenJDK 64-Bit Server VM (build 11.0.18+10-post-Debian-1deb11u1, mixed mode)

javac 11.0.18

Any ideas why this could be?

[Stamina Model Checker]

(Attached are the model files and an open virtual appliance for the VM we are using: https://usu.box.com/s/os1n4xp8reawv9svd66zjtqfsj9gip5k)

[Dave Parker]

Hi,

I don't see an immediately obvious cause for this, especially if the
model is small enough to fit in RAM comfortably, which it seems to be.
Is this out-of-the-box settings, i.e. hybrid engine? I'm happy to take a
look at the logs in case that helps.

Best wishes,

Dave

On 21/06/2023 22:08, Stamina Model Checker wrote:
> (Attached are the model files and an open virtual appliance for the VM
> we are using: https://usu.box.com/s/os1n4xp8reawv9svd66zjtqfsj9gip5k)
>
> On Wednesday, June 21, 2023 at 2:28:02 PM UTC-6 Stamina Model Checker wrote:
>
> We ran a few different models on the exact same version of PRISM
> with the same version of openJDK and openJRE on two different
> machines: one with a lot better specs than the other. The one with
> the better specs is an AMD Ryzen Threadripper with 128 GB RAM, and
> the one with the worse specs is a VM running on a host machine with
> an i7-8700 CPU and 16 GB RAM. The VM is allocated two to four cores
> of the CPU.
>
> In both cases, the model building took about the same amount of
> time, but the model checking was much faster on the VM (which has
> worse specs) than the original machine (which has better specs)
>
> For this model, we observed:
> 5m11.580s (311.58 s) on PRISM on Original Machine
> 3m31.887s (211.887 s) on PRISM on the VM
>

> *Versions:*

> PRISM: v4.5 (git tag)
> openjdk 11.0.18 2023-01-17
> OpenJDK Runtime Environment (build 11.0.18+10-post-Debian-1deb11u1)
> OpenJDK 64-Bit Server VM (build 11.0.18+10-post-Debian-1deb11u1,
> mixed mode)
> javac 11.0.18
>
> Any ideas why this could be?
>

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker-dev/238976c4-35aa-4464-b068-f9117ba81fe0n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker-dev/238976c4-35aa-4464-b068-f9117ba81fe0n%40googlegroups.com?utm_medium=email&utm_source=footer>.