ProB and MultiThread

[Laurent Payen]

Hi,

With the ProB API, we would like to run multiple validations in multiple Java threads to reduce execution time.

What is the best way to achieve this?

Is this solution the best for parallelizing the operations of several machines or can the ProB engine already be configured to parallelize its operations?

If not, what would be another way to do this with the best possible performance?

Thank you in advance for your help!

Best Regards

Laurent

[Michael Leuschel]

Hi Laurent,

sorry for the late reply.

The ProB Prolog core is single-threaded.
However, ProB also has a ZeroMQ extension which can be used for distributed model checking (https://prob.hhu.de/w/index.php?title=ParB).

I don’t think this can be accessed from the Java API.
In principle the Java API can also launch multiple ProB Prolog core processes.

What exactly would you like to run in parallel?

Greetings,
Michael

[Laurent Payen]

Thanks Michael for your answer.

We have thousands of machines to send to Prob and to minimize the time it takes to prove them, we would like to send them to multiple cores.

You say that the Java API can launch multiple ProB Prolog core processes, any example ?

Best regards

Laurent

[Michael Leuschel]

Hi,

I myself do not have an example.
I guess you should need to use Java’s concurrency features and keep multiple StateSpace objects (each of which will be associated with a different ProB Prolog process).
Greetings,
Michael