[LLVMdev] [RFC] Defining Infinite Loops

[Hal Finkel]

----- Original Message -----
> From: "Sanjoy Das" <sanjoy at playingwithpointers.com>
> To: "Philip Reames" <listmail at philipreames.com>
> Cc: "Chandler Carruth" <chandlerc at google.com>, "Hal Finkel" <hfinkel at anl.gov>, "LLVM Dev" <llvmdev at cs.uiuc.edu>
> Sent: Saturday, July 18, 2015 2:52:56 AM
> Subject: Re: [LLVMdev] [RFC] Defining Infinite Loops
> 
> > "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.

This does indeed sound like a good idea if we use metadata like this.

> 
> 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.

I think the problem is that this depends on the definition of your abstract machine. In Java, if you have a Thread you can query its state: it is observable whether it is still running or not. Many languages don't have abstract machines that contain such a notion, and so a thread not performing productive actions is indistinguishable from a thread not running at all. I think that, in terms of defining LLVM, we probably need to stick closer to this latter vantage point.

 -Hal

> 
> -- Sanjoy
> 

-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory