World's most popular travel blog for travel bloggers.

# [Solved]: How to prove if an algorithm is reentrant?

, ,
Problem Detail:

I think, maybe some formalism could exist for the task which makes it significantly easier.

My problem to solve is that I invented a reentrant algorithm for a task. It is relative simple (its pure logic is around 10 lines in C), but this 10 lines to construct was around 2 days to me. I am 99% sure that it is reentrant (which is not the same as thread-safe!), but the remaining 1% is already enough to disrupt my nights.

Of course I could start to do that on a naive way (using a formalized state space, initial conditions, elemental operations and end-conditions for that, etc.), but I think some type of formalism maybe exists which makes this significantly easier and shorter.

Proving the non-reentrancy is much easier, simply by showing a state where the end-conditions aren't fulfilled. But of course I constructed the algorithm so that I can't find a such state.

I have a strong impression, that it is an algorithmically undecidable problem in the general case (probably it can be reduced to the halting problem), but my single case isn't general.

I ask for ideas which make the proof easier. How are similar problems being solved in most cases? For example, a non-trivial condition whose fulfillment would decide the question into any direction, would be already a big help.

One approach is to design your code so it is "safe by construction", so re-entrant calls cannot happen. For instance, one way to do this is to use mutual exclusion to ensure that your method can't be invoked again while it is in the middle of running, to ensure you'll never have two instances running at the same time. For instance, this kind of approach is often used to ensure that interrupt handlers are correct: they often clear interrupts at the beginning and re-enable them at the end.

Another method is to take whatever code you already have and try to prove it will continue to function correctly even in the presence of re-entrant invocations. Here you can pick your favorite formal logic for reasoning about program correctness. For instance, you can use Hoare-style logic to specify the intended functionality and prove it correct. Then, you consider a tweaked version of your code, where before and after each statement, there is a (non-deterministic) possibility of a recursive invocation of the method being externally invoked; now you prove that the tweaked version continues to meet the spec. You can replace Hoare logic with any other method for program verification.