# Multicore model checking with Alloy

**URL:** <https://alloytools.discourse.group/t/multicore-model-checking-with-alloy/310>\
**Category:** Questions\
**Created:** [December 21, 2022, 11:20am UTC](https://alloytools.discourse.group/t/multicore-model-checking-with-alloy/310 "2022-12-21T11:20:28Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![ilkane](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ilkane/32/124_2.png) [@ilkane](https://alloytools.discourse.group/u/ilkane)\
**Post date:** [December 21, 2022, 11:20am UTC](https://alloytools.discourse.group/t/multicore-model-checking-with-alloy/310/1 "2022-12-21T11:20:28Z")

</div>

Is there something like high performance model checking using Alloy, something like assigning multiple cores to Alloy engine? Do you know any even experimental academic or industrial works that try to do this?

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [December 22, 2022, 8:00am UTC](https://alloytools.discourse.group/t/multicore-model-checking-with-alloy/310/2 "2022-12-22T08:00:02Z")

</div>

Alloy uses plugable solvers, see the menu. Some of these solvers use the parallelism available on a platform.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [December 22, 2022, 9:22am UTC](https://alloytools.discourse.group/t/multicore-model-checking-with-alloy/310/3 "2022-12-22T09:22:13Z")

</div>

Adding to Peter’s answer (e.g. the PLingeling solver), notice that Alloy (thanks to @nmacedo and @alcino) 6 is equipped with a “Decompose strategy” entry in the options menu. The strategy consists in choosing, or not, to consider a verification problem featuring static sigs and fields as one big _amagalmated_ problem (encompassing all possible instantiations for static sigs and fields) or as as many as possible _smaller_ subproblems (where each subproblem corresponds to one _pre-computed_ valuation of static sigs and fields, what we call a _configuration_).

- In the latter case, subproblems can be solved in parallel. In practice, the fully decomposed strategy can be very efficient for SAT problems as the said problems can be quite smaller than the amagalmated one.
- Conversely, for UNSAT problems, the amagalmated approach can be more relevant as the decomposed one may yield so many UNSAT subproblems that it may well be faster to just check one big problem.
- As a middle ground, you have the “hybrid” strategy which performs the decomposition but also keeps one core for the amagalmated problem