[LangRef] Define mustprogress attribute

[atmnpatel]

Summary

LLVM IR currently assumes some form of forward progress. This form is
not explicitly defined anywhere, and is the cause of miscompilations
in most languages that are not C++11 or later. This implicit forward progress
guarantee can not be opted out of on a function level nor on a loop
level. Languages such as C (C11 and later), C++ (pre-C++11), and Rust
have different forward progress requirements and this needs to be
evident in the IR.

Specifically, C11 and onwards (6.8.5, Paragraph 6) states that "An
iteration statement whose controlling expression is not a constant
expression, that performs no input/output operations, does not access
volatile objects, and performs no synchronization or atomic operations
in its body, controlling expression, or (in the case of for statement)
its expression-3, may be assumed by the implementation to terminate."
C++11 and onwards does not have this assumption, and instead assumes
that every thread must make progress as defined in [intro.progress] when
it comes to scheduling.

This was initially brought up in [0] as a bug, a solution was presented
in [1] which is the current workaround, and the predecessor to this
change was [2].

After defining a notion of forward progress for IR, there are two
options to address this:

1. Set the default to assuming Forward Progress and provide an opt-out for functions and an opt-in for loops.
2. Set the default to not assuming Forward Progress and provide an opt-in for functions, and an opt-in for loops.

Option 2) has been selected because only C++11 and onwards have a
forward progress requirement and it makes sense for them to opt-into it
via the defined mustprogress function attribute. The mustprogress
function attribute indicates that the function is required to make
forward progress as defined. This is sharply in contrast to the status
quo where this is implicitly assumed. In addition, willreturn implies mustprogress.

The background for why this definition was chosen is in [3] and for why
the option was chosen is in [4] and the corresponding thread(s). The implementation is in D85393, the
clang patch is in D86841, the LoopDeletion patch is in D86844, the
Inliner patches are in D87180 and D87262, and there will be more
incoming.

[0] https://bugs.llvm.org/show_bug.cgi?id=965#c25
[1] https://lists.llvm.org/pipermail/llvm-dev/2017-October/118558.html
[2] https://reviews.llvm.org/D65718
[3] https://lists.llvm.org/pipermail/llvm-dev/2020-September/144919.html
[4] https://lists.llvm.org/pipermail/llvm-dev/2020-September/145023.html

[jdoerfert]

There is some appeal in not over-specifying this. Arguably, we can make loop deletion and others aware of this on a function level. We can continue to delete readnone + X calls if they are not noprogress which is the default. Languages that want to keep noprogress everywhere need to mark all functions. Though, I haven't thought this all the way through. @RustFolks do you see this work for you assuming reasonable changes to the optimization passes to look for the attribute?

[RalfJung]

This attribute indicates that the function is guaranteed to not make progress

I don't think this is correct. I think the correct wording is "the function is *permitted* to not make progress, i.e., to run into an infinite loop without side-effects". (Ideally there's a definition of "progress" somewhere that we can reference.)

There is some appeal in not over-specifying this.

As someone who keeps running into problems where LLVM is underspecified, I don't think "overspecification" is a problem that we have here. ;)

[atmnpatel]

Flipped the semantics as per the comments, included a definition of progress from the C++ standard, could not find strict definitions anywhere else.

[jdoerfert]

I like the new wording and reference. Maybe just callees, unclear.

[atmnpatel]

Addressed comments.

[atmnpatel]

Changing name of function IR attribute from noprogress to mayprogress to make the semantics clearer in that if this attribute is applied to a function, it is now permitted to not make forward progress, but may still make forward progress as opposed to never making any forward progress which is what noprogress sounds like.

[jdoerfert]

llvm/docs/LangRef.rst

1964

Say that functions without this attribute are implicit `mustprogress` and required to make progress to put this into context.

[atmnpatel]

Address comments.

[RalfJung]

Shouldn't it be "maynotprogress" (or "maybenoprogress" or so)? *Every* function *may* progress, but only those with this marker are also allowed to not "make progress".

(Sorry I first posted this in the wrong review I think.)

[jdoerfert]

In D86233#2256076, @RalfJung wrote:

Shouldn't it be "maynotprogress" (or "maybenoprogress" or so)? *Every* function *may* progress, but only those with this marker are also allowed to not "make progress".

The way to read it is:
Every function *mustmakeprogress* unless it has the *mayprogress* attribute.

So "may" is either they do or they don't, both are fine.
And, "must" means they have to or UB.

[RalfJung]

In D86233#2256563, @jdoerfert wrote:

In D86233#2256076, @RalfJung wrote:

Shouldn't it be "maynotprogress" (or "maybenoprogress" or so)? *Every* function *may* progress, but only those with this marker are also allowed to not "make progress".

The way to read it is:
Every function *mustmakeprogress* unless it has the *mayprogress* attribute.

So "may" is either they do or they don't, both are fine.
And, "must" means they have to or UB.

I understand. But this is not how the word "may" is usually used. When I say "you may do X", that typically implies that usually, X is not a thing you may do.
This can certainly be explained away, but the first impression people are going to have before reading the docs is likely going to be wrong.

[hfinkel]

In D86233#2256648, @RalfJung wrote:

In D86233#2256563, @jdoerfert wrote:

In D86233#2256076, @RalfJung wrote:

Shouldn't it be "maynotprogress" (or "maybenoprogress" or so)? *Every* function *may* progress, but only those with this marker are also allowed to not "make progress".

The way to read it is:
Every function *mustmakeprogress* unless it has the *mayprogress* attribute.

So "may" is either they do or they don't, both are fine.
And, "must" means they have to or UB.

I understand. But this is not how the word "may" is usually used. When I say "you may do X", that typically implies that usually, X is not a thing you may do.
This can certainly be explained away, but the first impression people are going to have before reading the docs is likely going to be wrong.

I agree. maynotprogress is more self explanatory.

[jdoerfert]

In D86233#2256699, @hfinkel wrote:

In D86233#2256648, @RalfJung wrote:

I understand. But this is not how the word "may" is usually used. When I say "you may do X", that typically implies that usually, X is not a thing you may do.
This can certainly be explained away, but the first impression people are going to have before reading the docs is likely going to be wrong.

I agree. maynotprogress is more self explanatory.

It may do something, it may not do something, sure we can rename it.

[atmnpatel]

Renamed to maynotprogress.

[lebedev.ri]

FWIW maynotprogress reads worse to me, because my first interpretation/reading was if it progresses, it's ub, i.e. it may not (as in, shall not) progress instead of might not make progress

[hfinkel]

In D86233#2256872, @lebedev.ri wrote:

FWIW maynotprogress reads worse to me, because my first interpretation/reading was if it progresses, it's ub, i.e. it may not (as in, shall not) progress instead of might not make progress

Funny. I was just thinking about this too. We really want this to read "might not progress". Maybe we should just name it that. mightnotprogress. 'may' is just too ambiguous.

Atmn, sorry for the churn. Sometimes naming is hard ;)

[nikic]

Or might_not_progress while we're at it :) No requirement to squash the whitespace.

[hfinkel]

In D86233#2256908, @nikic wrote:

Or might_not_progress while we're at it :) No requirement to squash the whitespace.

True. Although we squash the whitespace for all other attributes. I don't really like it, and would prefer the underscores, but it would be different.

[hfinkel]

In D86233#2256909, @hfinkel wrote:

In D86233#2256908, @nikic wrote:

Or might_not_progress while we're at it :) No requirement to squash the whitespace.

True. Although we squash the whitespace for all other attributes. I don't really like it, and would prefer the underscores, but it would be different.

I take that back. We have null_pointer_is_valid, sanitize_address, etc. now. I also vote for the underscores.

[atmnpatel]

Updated the description based on conversations on the mailing lists.

[atmnpatel]

Flipped directions and a rename.

[efriedma]

Maybe worth noting somewhere that willreturn implies mustprogress.

[atmnpatel]

Sorry, it slipped. Anything else?

[atmnpatel]

Ping. Is this good to go?

[jdoerfert]

@nikic @lebedev.ri @efriedma I'm fine with (the slightly modified) wording below. If you are too I suggest we go ahead.

llvm/docs/LangRef.rst

1968

This attribute indicates that the function is required to return, unwind,
or interact with the environment in an observable way e.g. via a
volatile memory access, I/O, or other synchronization. 
The ``mustprogress`` attribute is intended to model the
requirements of the first section of `[intro.progress] of the C++
Standard <http://eel.is/c++draft/intro.progress>`_. This attribute does
not apply transitively to callees, that means a callee might not make progress.
Note that `willreturn` implies `mustprogress`.

[lebedev.ri]

No further comments from me, but i strongly like inline comment reword.

[atmnpatel]

Updated wording.

[nikic]

llvm/docs/LangRef.rst

1968

Some notes from my side:

• I'm not sure how to interpret the "does not apply to callees" part. If mustprogress function A calls not-mustprogress function B and B goes into an infinite loop, then A will not return, unwind or interact with the environment, thus violating the mustprogress contract. Now, the callee does not necessarily have to be mustprogress in general, but I believe it needs to progress for any invocation from a mustprogress function -- or not?
• I would explicitly state that violating the progress requirement results in undefined behavior.
• It may be worthwhile to explicitly mention that a non-interacting loop inside a mustprogress function can thus be assumed to terminate and may be removed. That would help clarify the practical effect setting this attribute has.

[jdoerfert]

llvm/docs/LangRef.rst

1968

I'm not sure how to interpret the "does not apply to callees" part. If mustprogress function A calls not-mustprogress function B and B goes into an infinite loop, then A will not return, unwind or interact with the environment, thus violating the mustprogress contract. Now, the callee does not necessarily have to be mustprogress in general, but I believe it needs to progress for any invocation from a mustprogress function -- or not?

Yes. That is the intention. If we come from the perspective that C++ has the mustprogress requirement, it has to hold for any statement, including a call to a function that may not progress. However, the statement (=call) has to make progress from the C++ side. This is the same as other attributes, let's say readonly (aka. pure). A function can have that attribute and call an arbitrary function. This is all good as long as the arbitrary function is readonly for this call site.

Do you have an idea how to clarify this in the wording? (Even though other attributes implicitly make this assumption as well.)

I would explicitly state that violating the progress requirement results in undefined behavior.

Sure. @atmnpatel

It may be worthwhile to explicitly mention that a non-interacting loop inside a mustprogress function can thus be assumed to terminate and may be removed. That would help clarify the practical effect setting this attribute has.

Sounds good to me. @atmnpatel

[atmnpatel]

Addressed comments, does this sound like an appropriate wording for the behavior wrt callees?

[nikic]

Thanks for the clarification wrt callees, this LGTM now.

llvm/docs/LangRef.rst

1968

Nit: "it is undefined behavior" -> "the behavior is undefined" (seems to be the phrasing used for other attributes).

[atmnpatel]

Updated wrt nit.

[jdoerfert]

Again minor wording suggestions, LGTM otherwise

llvm/docs/LangRef.rst

1972

...
As a consequence, a loop in a function with the `mustprogress` attribute can be assumed to terminate if it does not interact with the environment in an observable way, and terminating loops without side-effects can be removed. 
...
apply to
...

[efriedma]

LGTM

[efriedma]

llvm/docs/LangRef.rst

1967

Minor question: is it really a good idea to link to eel.is? Certainly it's a convenient resource, but it's not official; as far as I know, it's just someone's personal website.

[atmnpatel]

Removed unofficial link, I agree that an unofficial link isn't that much better than no link. Updated wording as well.

[atmnpatel]

Updated to include syntax modifications in the llvm/utils

[atmnpatel]

rebase.

[atmnpatel]

Rebase to fix buildkite build.

llvm/docs/LangRef.rst

``nocf_check``
     entity to fine grain the HW control flow protection mechanism. The flag
     is target independent and currently appertains to a function or function
     pointer.
 ``shadowcallstack``
     This attribute indicates that the ShadowCallStack checks are enabled for
     the function. The instrumentation checks that the return address for the
     function has not changed between the function prolog and epilog. It is
     currently x86_64-specific.
+``mustprogress``
+    This attribute indicates that the function is required to return, unwind,
+    or interact with the environment in an observable way e.g. via a volatile
+    memory access, I/O, or other synchronization.  The ``mustprogress``
+    attribute is intended to model the requirements of the first section of
+    [intro.progress] of the C++ Standard. As a consequence, a loop in a
+    function with the `mustprogress` attribute can be assumed to terminate if
+    it does not interact with the environment in an observable way, and
+    terminating loops without side-effects can be removed. If a `mustprogress`
+    function does not satisfy this contract, the behavior is undefined.  This
+    attribute does not apply transitively to callees, but does apply to call
+    sites within the function. Note that `willreturn` implies `mustprogress`. 
 
 Call Site Attributes
 ----------------------
 
 In addition to function attributes the following call site only
 attributes are supported:
 
 ``vector-function-abi-variant``

llvm/utils/emacs/llvm-mode.el

(let ((table (make-syntax-table)))
     table)
   "Syntax table used while in LLVM mode.")
 
 (defvar llvm-font-lock-keywords
   (list
    ;; Attributes
    `(,(regexp-opt
        '("alwaysinline" "argmemonly" "builtin" "cold" "convergent" "inaccessiblememonly"
-         "inaccessiblemem_or_argmemonly" "inlinehint" "jumptable" "minsize" "naked" "nobuiltin"
+         "inaccessiblemem_or_argmemonly" "inlinehint" "jumptable" "minsize" "mustprogress" "naked" "nobuiltin"
          "noduplicate" "nofree" "noimplicitfloat" "noinline" "nonlazybind" "noredzone" "noreturn"
          "norecurse" "noundef" "nounwind" "optnone" "optsize" "readnone" "readonly" "returns_twice"
          "speculatable" "ssp" "sspreq" "sspstrong" "safestack" "sanitize_address" "sanitize_hwaddress" "sanitize_memtag"
          "sanitize_thread" "sanitize_memory" "strictfp" "uwtable" "willreturn" "writeonly" "immarg") 'symbols) . font-lock-constant-face)
    ;; Variables
    '("%[-a-zA-Z$._][-a-zA-Z$._0-9]*" . font-lock-variable-name-face)
    ;; Labels
    '("[-a-zA-Z$._0-9]+:" . font-lock-variable-name-face)

llvm/utils/kate/llvm.xml

<list name="parameter-attributes">
       <item> nest </item>
     </list>
     <list name="function-attributes">
       <item> alignstack </item>
       <item> alwaysinline </item>
       <item> argmemonly </item>
       <item> convergent </item>
       <item> inlinehint </item>
+      <item> mustprogress </item>
       <item> naked </item>
       <item> nobuiltin </item>
       <item> noimplicitfloat </item>
       <item> noinline </item>
       <item> noredzone </item>
       <item> noreturn </item>
       <item> nounwind </item>
       <item> optnone </item>

llvm/utils/llvm.grm

  | optsize
  | ssp
  | sspreq
  | returns_twice
  | nonlazybind
  | sanitize_address
  | sanitize_thread
  | sanitize_memory
+ | mustprogress
  ;
 
 OptFuncAttrs  ::= + _ | OptFuncAttrs FuncAttr ;
 
 OptGC         ::= + _ | gc STRINGCONSTANT ;
 
 OptAlign      ::= + _ | align EUINT64VAL ;
 OptCAlign     ::= + _ | ^ "," align EUINT64VAL ;

llvm/utils/vim/syntax/llvm.vim

syn keyword llvmKeyword
       \ linkonce_odr
       \ localdynamic
       \ localexec
       \ local_unnamed_addr
       \ minsize
       \ module
       \ monotonic
       \ msp430_intrcc
+      \ mustprogress
       \ musttail
       \ naked
       \ nest
       \ noalias
       \ nobuiltin
       \ nocapture
       \ noimplicitfloat
       \ noinline

llvm/utils/vscode/llvm/syntaxes/ll.tmLanguage.yaml

- match: "\\bacq_rel\\b|\
             \\blinkonce_odr\\b|\
             \\blocaldynamic\\b|\
             \\blocalexec\\b|\
             \\blocal_unnamed_addr\\b|\
             \\bminsize\\b|\
             \\bmodule\\b|\
             \\bmonotonic\\b|\
             \\bmsp430_intrcc\\b|\
+            \\bmustprogress\\b|\
             \\bmusttail\\b|\
             \\bnaked\\b|\
             \\bnest\\b|\
             \\bnoalias\\b|\
             \\bnobuiltin\\b|\
             \\bnocapture\\b|\
             \\bnoimplicitfloat\\b|\
             \\bnoinline\\b|\