Parallel Alloy Analyzers

Question

I generate quite a lot of Alloys specs (* .als files). For the medium-sized problem that I am trying to solve, I created 1536 * .als files. To save time on running all these files, I used the Java concurrency API (in particular ExecutorCompletionService with Future ) to run n Alloy commands in parallel, where n is the number of available logical cores on the machine (in my case 4, for 2 processors with HyperThreading).

In this context, sometimes it happens that a command freezes and does not return any result within the “reasonable” delay that I set for 5 seconds, since each * .als is quite simple.

This is not clear to me

• Should a splice really be used in such a parallel / parallel context? (I would expect this to be possible, as my team relies on Module differences)
• How can I interrupt / stop a frozen command? My program can detect these frozen commands, then ignore them and finally redistribute them for a predetermined (maximum) number of attempts. The good news is that I always managed to run these 1536 commands, usually after several attempts. The bad news is that I usually end up “freezing” my PC (i.e. up to 4 cores up to 100%) after completing all these Alloy commands (note that my program (Eclipse plugin) does not end at this point and continues performance). Killing the JVM will unfreeze my computer, probably indicating that the frozen alloy is still working ...

For the code, I wrote some ugly tricks to try to recover when I ran into a freeze problem. But basically it looks ( more ):

 for(MyClass c : myClasses) { AlloyWrapper worker = new AlloyWrapper(c, ...); tasks.add(worker); ecs.submit(worker); } 

I measured the executor to use all the cores / physical threads available on the machine.

As for AlloyWrapper, it does this ( more ):

The enable shell basically generates input for Alloy (based on the information contained in MyClass) and calls

 Module world = CompUtil.parseEverything_fromFile(null, null, input.getAbsolutePath()); solution = TranslateAlloyToKodkod.execute_command(NOP, world.getAllReachableSigs(), world.getAllCommands().get(0), opt); 

Tell me if you need more information.