search

aronisstav / Concuerror

OFFICIAL REPOSITORY MOVED:
https://github.com/parapluu/Concuerror
BSD 2-Clause "Simplified" License
1 stars 0 forks source link

Fake PIDs within processes #4

Closed aronisstav closed 6 years ago

aronisstav commented 7 years ago

For true stateless model checking, identical schedulings must reach identical states. When exploring in parallel, "identical" processes must therefore have the same PIDs.

This can be done by instrumentation of the self() primitive. Due to its possible presence in guards, this is trickier than other primitives.

aronisstav commented 7 years ago

This depends on #3.

aronisstav commented 6 years ago

An alternative path has been decided, using slave nodes and trying to generate the 'same' PIDs on each.