# How to prove if an algorithm is reentrant?

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.

• Functions called by the main function don't need to be reentrant (it can help, of course), depending on where reentrant calls to the main function can take place and how the other functions are called. Conversely, a function can be non-reentrant even though it doesn't directly manipulate global variables and it only calls reentrant functions (consider a pair of functions store and load that modify a global variable atomically — each function is reentrant but store(); do_stuff(); load() is not reentrant). – Gilles 'SO- stop being evil' Sep 8 '15 at 7:43