Paper number: d1486r1 Topic: Contracts Author: John Lakos Email: jlakos@bloomberg.net Audience: EWG ~*~ IN SEARCH OF ~*~ United Amendment to Contracts Facility for C++20 John Lakos - Bloomberg LP Revised: Thursday, February 21, 2019 Abstract Contracts are already part of the current WP for C++20, yet there is a known defect (see section 1) that was introduced during transcription after Rapperswil. Despite our best efforts, agreement on how best to amend the wording in the WP remains elusive. This paper proposes that we start with the intersection of p1290r1 and p1429r0, using the agreed upon default levels (which fixes the defect), and then add back mutually agreeable features -- approved by consensus straw-poll votes, one by one -- until no more consensus agreement can be reached. This maximal intersection of agreement will then become the united consensus amendment that the preponderance of original coauthors implicitly (if not explicitly) support. 0. Revision History The material in sections 1-3 (apart from corrections) is essentially unchanged from d1486r0. Those who have read that version of this paper (or were present at Monday's EWG meeting) can safely skip directly to section 4. 1. Introduction The contracts facility adopted into the current working paper in Rapperswil this past June has a critical flaw that makes it inconsistent with the original (and current) intent of the overwhelming preponderance of the authors of p0542r5, the joint paper on which it is based. This defect was the result of a transcription error during the formal wording process in association with CWG. As worded, the WP suggests that a 'default'-level or 'audit'-level contract-checking statement (CCS) can have only three possible semantics (as defined in p1333r0): "check (never continue)" or "check (maybe continue) when enabled, and "assume" when disabled. Although the ability for contracts to be used for optimization purposes was a noted selling point of this language-based version of the facility (as compared with, say, n3604), the absence of runtime checking was never intended to imply assumption by default (without opting in). Between the Rapperswil (June'18) and San Diego (September'18) meetings, there was much discussion on the reflector regarding contracts. A preview of an omnibus "area" paper, describing the landscape of possible future extensions for contracts (that would become p1332r0), was released on the reflector prior to San Diego. During that meeting, it was agreed that the WP as worded was not desirable, but the drive-by fix to eliminate all assumption from runtime-checkable contracts left many (including several co-authors of p0542r5) feeling needlessly disenfranchised. Following San Diego, two distinct ways of addressing this issue -- p1290r0 (Garcia) and p1333r0 and p1334r0 (Berne & Lakos) -- were included in the October'18 post-meeting mailing, along with the long-term overview paper, p1332r0 (Berne, Burgers, Rosen, and Lakos) and another non-proposal, p1335r0 (Lakos), contrasting the approaches of Garcia and Berne et al. An almost unprecedented amount of discussion has since transpired -- both privately and on the reflector. Despite genuine best efforts on both sides, we remain unable to reach a consensus proposal on our own. The two current proposals to address the agreed-upon major defect (see above) as well as some other small tweaks are p1290r1 (Garcia) and p1429r0 (Berne & Lakos). Both papers have been refined and in some cases streamlined and simplified, but neither position has changed substantially since San Diego. The sad thing is that almost everyone using contracts would not care (or even know) about the dissimilarities embedded in these proposals. The main differences center around (1) how levels are mapped to specific semantics at translation time, and (2) whether it is possible for checks that continue after a failed predicate and checks that don't to coexist within the same TU. The former makes a difference for only those who care to distinguish (at translation time) between running checks that are reasonably fast and those that are not. The latter applies only to larger development efforts where some of the code has contract-checking in place in production, and management wants to add new, as of yet untried checks that might detect latent (yet heretofore "benign") defects. 2. Road Map It is, I think, everyone's position that we do not want to do anything that would compromise an ideal design in C++23, yet we all feel we must repair the defect that accidentally slipped into the WP in Rapperswil. To that end, we now propose starting by identifying the intersection of agreement between the two papers -- r1290r1 and r1429r0 -- and then making that the final, unified proposal that we can all endorse, knowing full well that the result may well lack features that are currently available even in the status quo. The next step would then be to add back features -- one by one -- during our EWG meeting on Monday, February 18, 2019, in Kona (taking straw-poll votes for guidance) until maximal consensus agreement is achieved. Finally, this intersection of agreement would be submitted as our consensus amendment to the WP for contracts in C++20. In particular, the initial starting point is to adopt the same (see p1335r0) default semantics (see p1334r0) for levels proposed in both p1290r1 and p1429r0: default="check (never continue)" audit="ignore" axiom="assume" <- As of 1486r1, we no longer agree on this. If we remove the ability to alter these defaults, the defect in the WP is eliminated and the straw polls -- (1) eliminating UB from 'default'-level and 'audit'-level CCSs, and (2) requiring it for 'axiom'-level CCSs -- taken in San Diego is achieved! Done! The next steps will be to consider (a) if and how we modify level semantics per TU and also (b) whether it is permissible to specify contract-checking statements with varying continuation semantics within a TU. Finally, it has been widely suggested that we add a TU-wide master "disable flag" for the entire contract-checking facility. We think such a flag makes sense anyway and will be absolutely necessary if we cannot come to agreement on precisely how the default semantics for the various CCS levels are to be overridden on the build line (for consumption during translation). 3. Next Steps After Meeting Monday in Kona, our plan is to take whatever we have agreed to, make that "intersection of agreement" the next revision of this paper, and submit it as our united contracts-amendment proposal for consideration by the greater C++ standards community. It is our hope that all of the coauthors of p0542r5 will join in getting as much of a loaf as we reasonably can under these difficult and tightly time-constrained circumstances. 4. So Monday happened. Now what? EWG met on Monday, February 18, 2019 for the remainder of the day after Plenary to discuss the two most recent versions of the competing proposals: p1290r2 -- Garcia (presentor) "Avoiding Undefined behavior in contracts" and Voutilainen p1429r0 -- Berne (presentor) "Contracts That Work" and Lakos After the lunch break, the two proposals were contrasted objectively -- both abstractly and in the context of a series of specific, increasingly complex REAL-WORLD examples. Nathan Myers then presented his proposal p1426r2 -- Myers (presentor) "Pull the Plug on Contracts?" to remove contracts from C++20 and start fresh. Some polls followed: Avoiding undefined behavior in contracts SF F N A SA 5 5 10 7 7 Contracts That Work SF F N A SA 4 17 2 5 6 Pull the Plug on Contracts? SF F N A SA 2 7 4 14 7 Although there was no clear consensus over status quo, a generally preferred direction emerged. On Tuesday, members of both camps and some "new blood" (other informed parties) conspired to sort out what turned out to be just a few differing "bones of contention" (statements, not questions -- questions will come later): 1. The best "default" semantic for the 'axiom'-level contract-checking stements (CCSs) should be: (a) "ignore" (b) "assume" (c) unspecified (or implementation defined) 2. The extent to which we should define in the standard the set of conforming (valid) combinations of three semantics [ "ignore", "assume", "check (never continue)", and "check (maybe continue)" ] -- (including their respective meanings a la p1333r0) that are already in the status quo -- for three respective CCS levels ['default', 'audit', and 'axiom' ]: (a) None at all. (b) Only for where the standard is required to provide alternative values -- e.g., just 'ignore' and 'assume' for the 'axiom' level: [ "check (never continue)", "ignore", "ignore" ], [ "check (never continue)", "ignore", "assume" ]. (c) All four -- e.g., for 'default' and 'audit'. [ "ignore", "ignore", "ignore" ], [ "assume", "ignore", "ignore" ], [ "check (never continue)", "ignore", "ignore" ], [ "check (maybe continue)", "ignore", "ignore" ], [ "ignore", "assume", "ignore" ], : : : `-----. : `-----------------------------. : `----------------------. : : : : [ "check (maybe continue)", "check (maybe continue)", "assume" ]. 3. The extent to which the standard should attempt to discourage compiler vendors from providing all 4 X 4 X 2 = 32 supportable combinations of contract-checking semantics: (a) Allow no changing from the defaults. (b) Allow changing only among the required subset of allowed combinations. (c) Allow changing from among only a yet-TBD subset of the 32 well-defined (p1333r0) and easily supportable combinations. (d) Allow changing from among any of the 32 possible combinations. 4. The extent to which we should restrict the manner in which compiler vendors obtain information from clients as to how semantics are associated with the three CCS levels: (a) not at all (b) expressed as independent level assignments (c) expressed as the animalization of a build level, a continuation mode, and an axiom mode (d) both 5. The intended use case of an 'axiom'-level CCS: (a) To be able to express a predicate that cannot be run (e.g., cannot be written, would take way too long even for the 'audit' level, or might cause a side-effect) knowing that any functions invoked from the predicate will never be run (and need not even have a definition in the program). -- Dos Reis, et al., p0380r0 Sat, May 28, 2016 (b) "An axiom states that something may be taken as a fact. If you don't want your compiler to use that fact for optimization, turn off axioms. Turning off axioms would (I assume :-)) affect only compilers/optimizers, rather than all static analysers/verifiers (those will do whatever is appropriate for them)." -- Bjarne Stroustrup on Wed, Feb 20, 2019 15:19 EST After especially careful consideration, we have developed a tentative, aggressively stripped-down version of p1429r0, which we are planning to distribute as d1429r1. This new proposal explicitly does NOT provide what any individual author wants, but does meet the anticipated (see p1332r0) needs of the overwhelming majority of likely users of a new contract-checking facility in C++20. =============================================================================== 1. Based on the above disagreement, we imagine four potential proposals for the (realistic) maximal intersection of agreement in the Kona timeframe. The proposal we plan to present to this body will depend on which variant(s) receives the strongest consensus: A. BATMAN SF F N A SA - one required set of level assignments: default="check (never continue)", audit="ignore", axiom="ignore" - no other detailed specification of conforming semantics in the WP. B. BATGIRL SF F N A SA - two required sets of level assignments: default="check (never continue)", audit="ignore", axiom="ignore" default="check (never continue)", audit="ignore", axiom="assume" Developers must be able to toggle between these two required sets. - no other detailed specification of conforming semantics in the WP. C. BATMAN and ROBIN SF F N A SA - one required set of level assignments: default="check (never continue)", audit="ignore", axiom="ignore" - All 32 combinations are explicitly conforming extensions. It is up to the compiler vendor to determine if and to what extent developers are allowed to remap level semantics subject to existing constraints. D. BATGIRL AND ROBIN SF F N A SA - two required sets of level assignments: default="check (never continue)", audit="ignore", axiom="ignore" default="check (never continue)", audit="ignore", axiom="assume" Developers must be able to toggle between these two required sets. - All 32 combinations are explicitly conforming extensions. It is up to the compiler vendor to determine if and to what extent developers are allowed to remap level semantics subject to existing constraints. =============================================================================== What follows is a series of polls to give all of us a sense of what people in the room feel. We are looking for the room's help, and we make no promises to act on this information (though -- knowing us -- we probably will). :) =============================================================================== 2. Assuming ROBIN came along for the ride (i.e., C or D above), which of the following additional REQUIREMENTS -- FROM the respective papers -- would you be most comfortable with defining in the standard. A. NO ADDITIONAL REQUIREMENT if BATMAN (1/32) else BATGIRL (2/32) SF F N A SA B. From p1290r1 -- i.e., build-level + cont. mode + axiom mode (10`/32) SF F N A SA C. From p1429r0 -- i.e., independent assignment (32/32) SF F N A SA D. From p1290r1 & p1429r0 -- i.e., Both direct/indirect mappings (32/32) SF F N A SA ------------------------------------------------------------------------------- 3. Should we come back with a paper proposing in-CCS semantics SF F N A SA ------------------------------------------------------------------------------- 4. Should we REQUIRE that all checks can be disabled? SF F N A SA ------------------------------------------------------------------------------- 5. Should we bring we bring back a paper reflecting the results SF F N A SA of polls 2-5 in in time for C++20. =============================================================================== In the course of trying to figure out what are the main problems with the current CCF, we seem to have discovered a HUGE problem in that the name that was chosen for the most infrequently used CCS-level, "axiom", is being widely misunderstood - even among the proposal authors -- and no amount of arguing seems likely to change that. Consider that neither [[ expects axiom: is_reachable(a, b) ]] nor __builtin_assume(is_reachable(a, b)) necessarily satisfies everyone's "classical" definition of "axiom". To fix this problem, we would like to rename the CCS-level label "axiom" to anything but E.g., [ ] abstract [ ] annotation [ ] comment [ ] compile-time [ ] conjecture [ ] faith [ ] hope [ ] hypotheses [ ] hypothetical [ ] ideal [ ] lemma [ ] not-runtime [ ] posit [ ] rhetorical [ ] speculate [ ] static [ ] theorem [ ] transcendent [ ] unavailable [ ] unchecked [ ] unevaluated as in [[ expects hope: is_reachable(a, b) ]] =============================================================================== Please check your favorite (or come up with an even better name than any of these) and think of it when you answer the following polls. 6. Should we try to replace "axiom" with a less confusing/controversial name? SF F N A SA ------------------------------------------------------------------------------- 7. Should we remove entirely axiom-level checks from the C++20 working paper? SF F N A SA =============================================================================== One last request for guidance from this group. =============================================================================== For those familiar with p1332r0, "Contract Checking in C++: (long-term Roadmap)" ONLY: 8 Should we bring back a proposal for "Roles" as defined in p1332r0? SF F N A SA 9. Should we bring them back at Cologne or later? SF F N A SA =============================================================================== Thanks to all for their kind advice. Mahalo!