In SICP 3.4.2 there is the problem of the order of events in the different processes.
Suppose we have two processes, one with three ordered events (a,b,c) and one with three ordered events (x,y,z). If the two processes run concurrently, with no constraints on how their execution is interleaved, then there are 20 different possible orderings for the events that are consistent with the individual orderings for the two processes.
As programmers designing this system, we would have to consider the effects of each of these 20 orderings and check that each behavior is acceptable. Such an approach rapidly becomes unwieldy as the numbers of processes and events increase.
Is there any tool / best practice which helps the programmer making sure every logically different cases are covered?
It would be nice if the programmer could define a set of events & constraints between them and the tool would return all the valid order of events (recognizing and grouping similar eg. looping patterns).
Given the list of possible event streams the programmer would be able to add/remove/modify the constraints.
The problem is important to me, because the most bug I have is related to some race condition or some not handled cases.
I don't really want to use a specific language with some advanced type system, I'd rather have a technology/language independent solution which acts as some kind of assistant - to design and document a system: with its events, constraints (and states).
It would be the holy grail to me.
I was searching for the solution across these topics: formal methods, formal verification, prolog (because of exhaustive search and logic), concurrency, dependent types, event-based programming, many types of testing, design by contract, cyclomatic complexity; but none of them gave me the answer. Furthermore, going deep into type theory seems to be an overkill.
"three ordered events (a,b,c)"
It depends on how much interleaving state exists and what resources need (during which time) to be shared. Check on books for Concurrency Theory for the full theory of languages. Somehow you need to formalize the dependencies of the processes [which again depend on code]
Race conditions and not handled cases can be reduced to scope and resources, so you broadly speaking you either need to limit your expressing possibilities to formally/automatically verify your codes w.r.t. according bug cases or you need limit resources.
In languages/on programming this is done for example via patterns, good APIs, language constructs etc. However there is no general feature and it depends on the use case.
Race conditions and unhandled cases look like you need stronger typing and automatic resource constraining or your software design might be flawed.