ProB and MultiThread

9 views
Skip to first unread message

Laurent Payen

unread,
Oct 12, 2023, 8:53:52 AM10/12/23
to ProB Users
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

unread,
Nov 16, 2023, 9:47:59 AM11/16/23
to Laurent Payen, ProB Users
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

unread,
Nov 16, 2023, 10:09:16 AM11/16/23
to Michael Leuschel, ProB Users
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

unread,
Nov 16, 2023, 10:28:22 AM11/16/23
to Laurent Payen, ProB Users, Jens Bendisposto
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
Reply all
Reply to author
Forward
0 new messages