How to prove if an algorithm is reentrant?

Question

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.

Answer 1

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.

Answer 2

If your function doesn't write to global variables or change items on the heap, it should be re-entrant. Also, look closely at the functions that your function calls to see if they are re-entrant. If you are modifying objects on the heap or global objects, look closely at if those objects are thread-safe. It's often easier to break the function into smaller functions that are obviously re-entrant. Then put locks around only the sections that might not be re-entrant. This often improves performance over having one big lock for the entire function. For instance, when adding an item to a global linked list: create the new item, fill the new item with data, put a lock on the list, add the item to the list, then release the lock. While you were creating the item, some other thread could be using the list.