[LLVMdev] [RFC] Defining Infinite Loops

[Sanjoy Das]

> "productive" (to steal Sanjoy's term)

Just to make it clear: this isn't something I came up with.  It is
used (perhaps not extensively) in describing co-inductive data
structures.  Insofar I understand the concept, it roughly means that
to get to a finite number of "things" (external actions, in our case)
you only have to execute a finite number of steps.

> What if we introduced a piece of branch (really, control transfer
> instruction) metadata (not loop) called "productive" (to steal Sanjoy's
> term) whose semantics are such that it can be assumed to only execute a
> finite number of times between productive actions (volatile,
> synchronization, io, etc..).  We then tag *all* branches emitted by Clang
> with this metadata. This gives us the benefit of the loop metadata in that a
> single tagged backedge branch implies a productive loop, but allows
> productive recursive functions to be converted into productive loops in a
> natural way.

I think this is a good idea.  However, I'll suggest one modification:
our specification of a "productive" control transfer should be that
only a finite number of *productive control transfers* can run between
productive actions (volatile write, IO etc.).  This is subtly
different from stating that any one productive control transfer
executes only a finite number of times between productive actions.

While discussing offline we decided that these were equivalent (and
theoretically they are), but this second definition lets simple local
CFG manipulation be more aggressive.  For instance, say you wish to
split an edge or a basic block.  With your definition, marking the
newly inserted branches as productive would involve proving that the
new branch is not part of an existing (well defined) infinite loop,
since inserting a productive branch in an otherwise well-defined
infinite loop will introduce UB.  However, if we go with this second
definition, we can (aggressively) mark the newly inserted branches as
productive, as long as they themselves do not introduce a cycle.

Another way of phrasing my suggestion is that any infinite "loop" that
does not do (IO / volatile memory access / atomic operations) has to
have at least one non-productive control transfer.  A "loop" in this
definition has to be general enough to encompass all possible control
flow transfer mechanisms (so mutual recursion will have to count as
"loop"ing, for whatever definition we come up for a loop).

The only thing that bugs me about this notion of "productivity" (both
your idea and mine) is that, going by the Java spec, it isn't that a
thread stalled in an infinite loop is not performing any actions; but
the stalling is itself an "external" action (similar to writing to a
socket or program termination).  It would be nice if it were possible
to precisely capture that.

-- Sanjoy