P1494 R4 Partial program correctness

wg21bot commented 5 years ago

P1494R0 Partial program correctness (S. Davis Herring)

jensmaurer commented 5 years ago

This seems to be EWG territory first.

tituswinters commented 5 years ago

Seems to be EWG territory, not library.

opensdh commented 5 years ago

@tituswinters: It does add a library function. I make no claim that the name is so good that LEWG doesn't want to change it. That said, surely EWG should see it first.

opensdh commented 5 years ago

Given recent news, I should point out that it is useful in the absence of contracts.

opensdh commented 5 years ago

@jensmaurer: Should this in fact be closed (given my previous comment)?

jensmaurer commented 5 years ago

Agreed. I've removed the "contracts" label and re-opened the issue.

wg21bot commented 5 years ago

P1494R1 Partial program correctness (S. Davis Herring)

jfbastien commented 5 years ago

Even if this isn't contracts-specific, I'd like SG21 to review it first and forward to EWG.

jfbastien commented 4 years ago

Moving to EWG after discussion with SG21 chair. Actually, I talked to @ogiroux and SG1 wants to see it first, because It's Complicated.

ogiroux commented 3 years ago

We discussed this paper this week. SG1 noted a few things will want to see in a final version of this paper, as noted in the minutes, but that needn't block its progress. Will reassign to EWG.

jensmaurer commented 3 years ago

Adding SG21 and SG22 for information, as discussed by EWG 2021-11-04.

erichkeane commented 3 years ago

EWG Discussed D1494R2 in the November 4th, 2021 meeting.

The following poll was taken:

EWG approves D1494R2 for forwarding to Electronic Polling for forwarding to Core for inclusion into C++23 pending LEWG approval.

SF	F	N	A	SA
5	7	0	0	0

Result: Consensus

We also encourage SG21, and SG22 to take a look as well.

wg21bot commented 2 years ago

P1494R2 Partial program correctness (S. Davis Herring)

AaronBallman commented 2 years ago

This paper was discussed at the Dec 2021 SG22 meeting.

Poll: SG22 does not see any compatibility concerns for the direction of P1494r2. Attendees: 11 (though Aaron had stepped away) No objection to unanimous consent.

Removing the SG22 tag.

ben-craig commented 2 years ago

P1494R2: Partial program correctness

2022-02-01 Library Evolution Telecon Minutes

Chair: Ben Craig

Champion: Davis Herring

Minute Taker: Inbal Levi

SUMMARY: This facility is in the middle of polling by EWG, but since it touches library, it needs LEWG oversight. A request was made to add the new function to freestanding.

OUTCOME:

POLL: Modify P1494R2 (Partial program correctness) by adding std::observable to freestanding, and then send the revised paper to CWG for C++23 classified as priority P3 (no electronic poll).

Strongly Favor	Weakly Favor	Neutral	Weakly Against	Strongly Against
11	9	2	0	0

Attendance: 34

# of Authors: 1

Author Position: SF

Outcome: Strong Consensus

jfbastien commented 2 years ago

2022-02 poll results:

SF	F	N	A	SA
10	7	3	4	1

Abstain: 20

Poll outcome:❌ no consensus

wg21bot commented 5 months ago

P1494R3 Partial program correctness (S. Davis Herring)

jfbastien commented 4 months ago

Discussed in St Louis today during the contracts discussion.

Poll: P1494R3 — Partial program correctness, forward to LEWG and CWG for inclusion in C++26. Note that we might revisit this paper, as Andrew Tomazos has promised to provide a C++ version of WG14’s N3128 which might bring new information regarding P1494.

| SF | F | N | A | SA | | 9 | 14 | 4 | 4 | 0 |

Result: consensus.

opensdh commented 4 months ago

@ben-craig: While R2 was approved by LEWG already, I want to make it clear that R3 contains new information that it might want to consider.

ogiroux commented 4 months ago

SG1 too. :)

jensmaurer commented 4 months ago

CWG 2024-06-25 in St. Louis: Reviewed, needs updates.

inbal2l commented 4 months ago

@ben-craig: While R2 was approved by LEWG already, I want to make it clear that R3 contains new information that it might want to consider.

@opensdh for future reference - would be good to tag me as well, as I'm mostly the one in charge of setting our schedule so I need to know this waits for us. Scheduled for our second upcoming telecon.

ben-craig commented 3 months ago

2024-08-06 Library Evolution Telecon

P1494R3: Partial program correctness

2024-08-06 Library Evolution Telecon Minutes

Champion: Davis Herring Chair: Ben Craig Minute Taker: Mark Hoemmen

Summary

POLL: Make standard-library functions that deliver data to the host environment to be written to a file (including the terminal) be observable checkpoints (reflects what C did).

SF	WF	N	WA	SA
6	7	3	0	0

Attendance: 20

# of Authors: 1

Author Position: WF

Outcome: Strong consensus in favor

Comments:

POLL: Make breakpoint and breakpoint_if_debugging observable checkpoints.

SF	WF	N	WA	SA
4	8	0	2	2

Attendance: 20

# of Authors: 1

Author Position: WA

Outcome: Consensus in favor

Comments: SA: breakpoint is specified as having impl defined semantics, don't need to say anymore WA: I don't believe that defining these as observable checkpoints has any semantics at all, belive that this is subsumed by the first poll

POLL: (retake after comments made above) Make breakpoint and breakpoint_if_debugging observable checkpoints.

SF	WF	N	WA	SA
2	5	2	5	2

Attendance: 19

# of Authors: 1

Author Position: WA

Outcome: No consensus for change

Comments:

POLL: LEWG requests that EWG consider making volatile accesses observable checkpoints (this would match the C proposal)

SF	WF	N	WA	SA
5	5	4	1	1

Attendance: 18

# of Authors: 1

Author Position: N

Outcome: Consensus in favor

Comments: WA: might affect optimizations more than i/o, would like to see more research. SA: Sympathetic to the idea, not convinced that this couldn't just be handled by implementations.

POLL: Remove std::observable from P1494, knowing that volatile accesses are not observable checkpoints in the current revision of P1494

SF	WF	N	WA	SA
1	4	7	3	1

Attendance: 18

# of Authors: 1

Author Position: N

Outcome: No consensus for change

Comments: SA: Volatile I/O is important for freestanding platforms, and we need some way to bound undefined behavior in freestanding environments.

Next Steps

Come back with a revision that adds the I/O checkpoint wording. Go to EWG and get a poll about volatile accesses. @jfbastien

wg21bot commented 1 month ago

P1494R4 Partial program correctness (S. Davis Herring)

jfbastien commented 1 week ago

See:

cplusplus / papers