Editorial: Use abstract closures instead of semantic functions #1907

syg · 2020-03-20T21:32:19Z

Refactor semantic functions as used by atomic RMW operations to be
a subclass of abstract closures that are pure.

The remaining use of "semantic function" for reads-bytes-from is
changed to say "mathematical function". It is used in the axiomatic
event semantics and do not have algorithm steps.

Fixes #1895.

spec.html

ljharb · 2020-03-21T21:27:23Z

spec.html

+          1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).
+          1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).
+          1. Let _T_ be Type(_x_).
+          1. Let _sum_ be _T_::add(_x_, _y_).


Suggested change

1. Let _sum_ be _T_::add(_x_, _y_).

1. Let _sum_ be ! _T_::add(_x_, _y_).

this one isn't an abstract closure.

That's true, that's worth a note saying none of the steps performed by ::add here are observable because x and y are guaranteed to be numbers.

which means that "doesn't call other abstract operations" isn't actually necessary to indicate or guarantee that something is "pure" - so why is that part of the definition of these functions?

spec.html

ljharb · 2020-03-21T21:29:16Z

spec.html

      <p>The following steps are taken:</p>
      <emu-alg>
-        1. Return ? AtomicReadModifyWrite(_typedArray_, _index_, _value_, `or`).
+        1. Let _or_ be a new read-modify-write modification function with parameters (_xBytes_, _yBytes_) that captures nothing and performs the following steps atomically when called:
+          1. Return ByteListBitwiseOp(`|`, _xBytes_, _yBytes_).


Suggested change

1. Return ByteListBitwiseOp(`|`, _xBytes_, _yBytes_).

1. Return ! ByteListBitwiseOp(`|`, _xBytes_, _yBytes_).

ljharb · 2020-03-21T21:29:41Z

spec.html

+        1. Let _subtract_ be a new read-modify-write modification function with parameters (_xBytes_, _yBytes_) that captures _type_ and _isLittleEndian_ and performs the following steps atomically when called:
+          1. Assert: _xBytes_ and _yBytes_ have equal length.
+          1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).
+          1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).


Suggested change

1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).

1. Let _y_ be ! RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).

ljharb · 2020-03-21T21:29:47Z

spec.html

-        1. Return ? AtomicReadModifyWrite(_typedArray_, _index_, _value_, `subtract`).
+        1. Let _subtract_ be a new read-modify-write modification function with parameters (_xBytes_, _yBytes_) that captures _type_ and _isLittleEndian_ and performs the following steps atomically when called:
+          1. Assert: _xBytes_ and _yBytes_ have equal length.
+          1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).


Suggested change

1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).

1. Let _x_ be ! RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).

ljharb · 2020-03-21T21:30:08Z

spec.html

+          1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).
+          1. Let _T_ be Type(_x_).
+          1. Let _difference_ be _T_::subtract(_x_, _y_).
+          1. Return NumericToRawBytes(_type_, _differenceBytes_, _isLittleEndian_).


Suggested change

1. Return NumericToRawBytes(_type_, _differenceBytes_, _isLittleEndian_).

1. Return ! NumericToRawBytes(_type_, _differenceBytes_, _isLittleEndian_).

ljharb · 2020-03-21T21:30:18Z

spec.html

      <p>The following steps are taken:</p>
      <emu-alg>
-        1. Return ? AtomicReadModifyWrite(_typedArray_, _index_, _value_, `xor`).
+        1. Let _xor_ be a new read-modify-write modification function with parameters (_xBytes_, _yBytes_) that captures nothing and performs the following steps atomically when called:
+          1. Return ByteListBitwiseOp(`^`, _xBytes_, _yBytes_).


Suggested change

1. Return ByteListBitwiseOp(`^`, _xBytes_, _yBytes_).

1. Return ! ByteListBitwiseOp(`^`, _xBytes_, _yBytes_).

syg · 2020-03-23T17:35:11Z

I'm fine with requiring either that no ?/! be used anywhere in the RMW modification functions, or that only ! be used. I prefer the former, since I think it's more obvious to me that the function is "pure" that way. @ljharb I assume prefers the other way. @bakkot tie-breaker?

bakkot · 2020-03-23T17:43:06Z

My preference is also to avoid !. I hope to address #1796 this week, at which point avoiding ! will be unambiguously the right thing.

ljharb · 2020-03-23T18:24:24Z

Prior to #1796, the reigning approach is to always use the !. To me, purity has nothing to do with completion record vs return value (#1907 (comment)).

syg · 2020-03-23T18:36:15Z

[...] but with the current state of completion values, having some of them not return one seems very confusing to me.

The current state is not consistent, as we've discussed at length before, and besides @bakkot will PR that.

To me, purity has nothing to do with completion record vs return value (#1907 (comment))

This is the wrong intuition and this confusion is precisely why @bakkot, @michaelficarra, and I want to do the reform. Completion Records are about reifying control in observable program evaluation, with normal meaning "next step", return meaning early returns, break meaning labeled statement breaks, and continue meaning loop continues.

! Op() means "Op can have effects on evaluation control flow. For this particular callsite, the only effect it can have is a normal continuation, i.e. evaluate the next thing."
? Op() means "Op can have effects on evaluation control flow. For this particular callsite, abrupt values are propagated immediately."
Op() means "Op cannot have effects on evaluation control flow."

1 and 3 really should not be conflated. 3 tells me a lot about no observability on control flow, which is a necessary (but not sufficient) condition for an operation being observable at all. 1 doesn't tell me that.

Edit: That's what ?/! should mean post-reform. For now we just have an inconsistent state, but I prefer to not perpetuate what I consider a wrong intuition by having ! in the newer parts of the spec that are meant to not have observable effects on control flow.

spec.html

ljharb · 2020-03-23T18:37:23Z

spec.html

+          1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).
+          1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).
+          1. Let _T_ be Type(_x_).
+          1. Let _sum_ be _T_::add(_x_, _y_).


this one isn't an abstract closure.

ljharb · 2020-03-23T18:40:23Z

The problem I see is that step 2 is one that's easy to forget, and the omnipresence of ! helps ensure that a ? is not omitted. This is something we should really discuss re the overall reform topic tho; however pending that, i don't think we should be changing the way callable things work in the spec so far. (it is pretty consistent already, i think, just not desirable in the long term)

spec.html

ljharb · 2020-03-24T03:50:36Z

spec.html

+        <li>Their individual algorithm steps are not observable.</li>
+      </ul>
+      <emu-note>
+        <p>To aid verifying that a read-modify-write modification function's algorithm steps constitute a pure, mathematical function, the following editorial conventions are recommended:</p>


thanks, this is much clearer to me.

spec.html

syg · 2020-03-25T00:01:21Z

Addressed review, squashed, rebased.

ljharb · 2020-03-28T22:11:38Z

spec.html

+    <emu-clause id="sec-arraybuffer-notation">
+      <h1>Notation</h1>
+      <p>The descriptions below in this section, <emu-xref href="#sec-atomics-object"></emu-xref>, and <emu-xref href="#sec-memory-model"></emu-xref> use the read-modify-write modification function internal data structure.</p>
+      <p>A <dfn>read-modify-write modification function</dfn> is a mathematical function that is notationally represented as an abstract closure that takes two Lists of bytes as arguments and returns a List of bytes. These abstract closures satisfy all of the following properties:</p>


Suggested change

<p>A <dfn>read-modify-write modification function</dfn> is a mathematical function that is notationally represented as an abstract closure that takes two Lists of bytes as arguments and returns a List of bytes. These abstract closures satisfy all of the following properties:</p>

<p>A <dfn>read-modify-write modification function</dfn> is a mathematical function that is notationally represented as an abstract closure that takes two Lists of byte values as arguments and returns a List of byte values. These abstract closures satisfy all of the following properties:</p>

syg · 2020-05-07T00:06:01Z

Rebased; PTAL.

spec.html

bakkot

This still LGTM.

…1907) Refactor semantic functions as used by atomic RMW operations to be a subclass of abstract closures that are pure. The remaining use of "semantic function" for reads-bytes-from is changed to say "mathematical function". It is used in the axiomatic event semantics and do not have algorithm steps. Fixes tc39#1895.

syg requested a review from a team March 20, 2020 21:32

syg force-pushed the semantic-functions-to-abstract-closures branch from 990730d to a810c60 Compare March 20, 2020 21:33

syg added the editorial change label Mar 20, 2020

bakkot reviewed Mar 20, 2020

View reviewed changes

spec.html Show resolved Hide resolved

bakkot reviewed Mar 20, 2020

View reviewed changes

spec.html Show resolved Hide resolved

bakkot reviewed Mar 20, 2020

View reviewed changes

spec.html Outdated Show resolved Hide resolved

bakkot reviewed Mar 20, 2020

View reviewed changes

spec.html Show resolved Hide resolved

ljharb reviewed Mar 21, 2020

View reviewed changes

ljharb reviewed Mar 23, 2020

View reviewed changes

syg force-pushed the semantic-functions-to-abstract-closures branch from a19a3eb to 40dbfb4 Compare March 23, 2020 20:39

ljharb reviewed Mar 24, 2020

View reviewed changes

syg force-pushed the semantic-functions-to-abstract-closures branch from 40dbfb4 to 6fa3b1a Compare March 25, 2020 00:00

ljharb approved these changes Mar 28, 2020

View reviewed changes

ljharb requested a review from michaelficarra March 28, 2020 22:12

ljharb self-assigned this Mar 28, 2020

ljharb requested review from bakkot and a team March 28, 2020 22:12

syg force-pushed the semantic-functions-to-abstract-closures branch from 6fa3b1a to ca1fb57 Compare May 7, 2020 00:05

jmdyck mentioned this pull request May 7, 2020

Sorting out completion records #1796

Closed

bakkot reviewed May 9, 2020

View reviewed changes

spec.html Show resolved Hide resolved

bakkot approved these changes May 9, 2020

View reviewed changes

ljharb changed the title ~~Editorial: Use abstract closures instead of semantic functions (#1895)~~ Editorial: Use abstract closures instead of semantic functions May 9, 2020

ljharb pushed a commit to syg/ecma262 that referenced this pull request May 9, 2020

Editorial: Add a sentence in Data Blocks about bytes (tc39#1907)

56bd5fc

ljharb force-pushed the semantic-functions-to-abstract-closures branch 2 times, most recently from 56bd5fc to 5370c6c Compare May 9, 2020 22:07

ljharb merged commit 5370c6c into tc39:master May 9, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Editorial: Use abstract closures instead of semantic functions #1907

Editorial: Use abstract closures instead of semantic functions #1907

syg commented Mar 20, 2020 •

edited by ljharb

Loading

ljharb Mar 21, 2020

ljharb Mar 23, 2020

syg Mar 23, 2020

ljharb Mar 23, 2020

ljharb Mar 21, 2020

ljharb Mar 21, 2020

ljharb Mar 21, 2020

ljharb Mar 21, 2020

ljharb Mar 21, 2020

syg commented Mar 23, 2020

bakkot commented Mar 23, 2020

ljharb commented Mar 23, 2020

syg commented Mar 23, 2020 •

edited

Loading

ljharb Mar 23, 2020

ljharb commented Mar 23, 2020

ljharb Mar 24, 2020

syg commented Mar 25, 2020

ljharb Mar 28, 2020

syg commented May 7, 2020

bakkot left a comment

	1. Let _sum_ be _T_::add(_x_, _y_).
	1. Let _sum_ be ! _T_::add(_x_, _y_).

	1. Return ByteListBitwiseOp(`\|`, _xBytes_, _yBytes_).
	1. Return ! ByteListBitwiseOp(`\|`, _xBytes_, _yBytes_).

	1. Let _y_ be RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).
	1. Let _y_ be ! RawBytesToNumeric(_type_, _yBytes_, _isLittleEndian_).

	1. Let _x_ be RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).
	1. Let _x_ be ! RawBytesToNumeric(_type_, _xBytes_, _isLittleEndian_).

	1. Return NumericToRawBytes(_type_, _differenceBytes_, _isLittleEndian_).
	1. Return ! NumericToRawBytes(_type_, _differenceBytes_, _isLittleEndian_).

	1. Return ByteListBitwiseOp(`^`, _xBytes_, _yBytes_).
	1. Return ! ByteListBitwiseOp(`^`, _xBytes_, _yBytes_).

	<p>A <dfn>read-modify-write modification function</dfn> is a mathematical function that is notationally represented as an abstract closure that takes two Lists of bytes as arguments and returns a List of bytes. These abstract closures satisfy all of the following properties:</p>
	<p>A <dfn>read-modify-write modification function</dfn> is a mathematical function that is notationally represented as an abstract closure that takes two Lists of byte values as arguments and returns a List of byte values. These abstract closures satisfy all of the following properties:</p>

Editorial: Use abstract closures instead of semantic functions #1907

Editorial: Use abstract closures instead of semantic functions #1907

Conversation

syg commented Mar 20, 2020 • edited by ljharb Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

syg commented Mar 23, 2020

bakkot commented Mar 23, 2020

ljharb commented Mar 23, 2020

syg commented Mar 23, 2020 • edited Loading

Choose a reason for hiding this comment

ljharb commented Mar 23, 2020

Choose a reason for hiding this comment

syg commented Mar 25, 2020

Choose a reason for hiding this comment

syg commented May 7, 2020

bakkot left a comment

Choose a reason for hiding this comment

syg commented Mar 20, 2020 •

edited by ljharb

Loading

syg commented Mar 23, 2020 •

edited

Loading