Include Extern specification #73

macrologist · 2024-02-20T20:16:16Z

This PR extends the spec to include new syntax to support the declaration and use of extern functions, synthesizing the discussion surrounding the RFC in #69.

erichulburd

I don't see any blockers, I think this is pretty ready to go.

erichulburd · 2024-03-28T17:16:44Z

specgen/spec/sec-other.s

+    PRAGMA EXTERN @ms{Identifier} "@ms{Extern Signature}"
+}
+
+@syntax[:name "Extern Signature"]{


erichulburd · 2024-03-28T17:19:51Z

specgen/spec/sec-other.s

+}
+
+@syntax[:name "Extern Parameter"]{
+    @ms{Identifier} : @rep[:min 0 :max 1]{mut} @ms{Type}


Just calling out this requires parameter names. I don't view that as a hard requirement for this spec change, but neither am I opposed to it.

I think it does deserve a bit of exposition, such as:

Quil requires the type signature to name all extern function parameters. This adds in program readability and debugging.

erichulburd · 2024-03-28T17:24:38Z

specgen/spec/sec-other.s

+@p{Declared externs may be appear in call instructions.  The precise
+meaning of an extern call is left up to the implementor.  From the
+perspective of the abstract machine, a call to an external function
+increments the program counter and has some effect on classical


I would suggest rephrasing this:

a call to an extern function will result in advancement of the program counter...

This is a bit nit-picky, but my concern is that the original wording implies the extern function itself controls and modifies the program counter, whereas from the POV of a hardware control system, the extern function just executes, something else at a higher level may be controlling the program counter.

erichulburd · 2024-03-28T17:30:33Z

specgen/spec/sec-other.s

+CALL rng num 10
+}
+
+@p{is roughly the same as}


@p{is the same as}

or

@p{is equivalent to}

kalzoo

Great to see it, thanks for writing this up.

What about overrides and subsequent re-declarations? On that, my suggestion would be to let the latest declaration win and to allow repeated EXTERN; that's compatible with the prepending of calibrations used in practice with Quil-T. All Quil-T instructions may be duplicated and the latest wins in case of conflict.

Alternatively, we could require that duplicates are okay only when identical; that is, functions could not be declared with two different signatures.

kalzoo · 2024-03-28T18:03:51Z

specgen/quil.lisp

@@ -229,7 +229,7 @@
  (let ((doc (make-instance 'document
               :title "Quil Specification"
               :author "Robert S. Smith; Rigetti & Co. Inc.; and contributors"
-               :version "2021.1 (DRAFT)"
+               :version "2024.1 (DRAFT)"


should we take out of draft given that it's in production use? It may (does) still have errors, but that's the nature of it

We'll update this in a later commit, and yes remove the draft

kalzoo · 2024-03-28T18:05:22Z

specgen/spec/sec-other.s

+E.g. the following are equivalent:}
+
+@clist{
+PRAMGA EXTERN rng "INTEGER (seed : INTEGER)"


Suggested change

PRAMGA EXTERN rng "INTEGER (seed : INTEGER)"

PRAGMA EXTERN rng "INTEGER (seed : INTEGER)"

kalzoo · 2024-03-28T18:06:13Z

specgen/spec/sec-other.s

+@p{is roughly the same as}
+
+@clist{
+PRAMGA EXTERN rng "(out : mut INTEGER, seed : INTEGER)"


Suggested change

PRAMGA EXTERN rng "(out : mut INTEGER, seed : INTEGER)"

PRAGMA EXTERN rng "(out : mut INTEGER, seed : INTEGER)"

kalzoo · 2024-03-28T18:09:39Z

specgen/spec/sec-other.s

+@p{Extern calls may appear in arithmetic expressions with some
+restrictions: the extern MUST have a known function signature, which
+MUST include a return type, and which MUST NOT include any mutable
+parameters.}


It must specifically return a single real value, right? I mention "real" here in light of the upcoming discussion on custom types

Why must it return a real value? Expressions are also used in matrix lines, which may be used in DEFWAVEFORM, so it could be useful to have a complex return type, right?

I'd maybe even go a step further - regardless as to current utility, design intent is clearer if the extern functions can return any type; it's the support for expressions that is the current / practical constraint here.

kalzoo · 2024-03-28T18:11:31Z

specgen/spec/sec-structure.s

@@ -125,7 +125,7 @@ i pi
 ADD AND AS CONTROLLED CONVERT DAGGER DECLARE DEFCIRCUIT DEFGATE DIV EQ
 EXCHANGE FORKED GE GT HALT INCLUDE IOR JUMP JUMP-UNLESS JUMP-WHEN
 LABEL LE LOAD LT MATRIX MEASURE MOVE MUL NEG NOP NOT OFFSET PAULI-SUM
-PERMUTATION PRAGMA RESET SHARING STORE SUB WAIT XOR
+PERMUTATION PRAGMA RESET SHARING STORE SUB WAIT XOR EXTERN CALL


I think we're all on board, but just for the record, this makes this a breaking change, something which is not expressed anywhere in the spec or the nature of quil (e.g. the spec version number does not communicate that, and the program itself does not carry its version)

I'd be in favor of a Quil version declaration. It could default to the last version that didn't support it. For example:

VERSION '2024.1' # otherwise assumed to be `2021.1` # ... etc

kalzoo · 2024-03-28T18:14:56Z

specgen/spec/sec-other.s

+@subsubsection[:title "Extern Signature Pragmas"]
+
+@p{Under some circumstances it may be desirable to specify the
+function signature of an external function. Signature declarations are
+supplied by way of a special pragma.}


Perhaps from earlier discussions, but I've missed why we're making the signature optional.

It's required when used in expressions but not when used with CALL, and I'm unclear on why we would treat those differently since they seem to share concerns

A CALL has an effect on the abstract machine. The type signature of a function passed to a CALL does not alter the meaning of the CALL as pertains to the abstract machine in terms of which Quil's semantics are defined. (the QAM has no way of knowing what an extern function does.) So type signatures are rightly specified in PRAGMAs - that is, their presence does not have an effect on the semantics of the program.

However, in the interests of keeping all our toes firmly affixed to the fronts of our feet, the footgun of value-mutating externs appearing inside expressions has been explicitly disallowed.

In some compilation steps expressions can be copied (in say, gate parameter positions). If an expression mutates the memory on which it operates, then copies of that expression are no longer guaranteed to have equivalent evaluations, which would break compilation.

kalzoo · 2024-03-28T18:15:14Z

specgen/spec/sec-other.s

+@subsubsection[:title "Externs in Arithmetic Expressions"]
+
+@p{Extern calls may appear in arithmetic expressions with some
+restrictions: the extern MUST have a known function signature, which


Suggested change

restrictions: the extern MUST have a known function signature, which

restrictions: the extern MUST have a declared function signature, which

kalzoo · 2024-03-28T18:18:04Z

specgen/spec/sec-other.s

+}
+
+
+@subsubsection[:title "Externs in Arithmetic Expressions"]


Can we use this opportunity to remove the baked-in-but-not-explicitly-enumerated functions from the spec and state that all functions in expressions must be declared?

Since that could make for a hard cutover, we could state that Quil implicitly declares that list of functions, and then state their PRAGMA EXTERN and EXTERNs

I'm more or less on board but it should be addressed more widely than in a comment to a PR before we make it explicit. I think we want to publish the "2024.1" spec version in the next month or so.

erichulburd · 2024-03-29T18:00:59Z

Alternatively, we could require that duplicates are okay only when identical; that is, functions could not be declared with two different signatures.

There's a discussion RE: function resolution here: #69 (comment)

I'm partial to overloading as long as resolution behavior is well defined. The idea would be programs could declare, for instance, RAND(mut seed : INTEGER) and RAND(mut seed : REAL), rather than RAND-INTEGER and RAND-REAL separately.

macrologist added 3 commits February 20, 2024 12:08

Include Extern specification

ee8a886

Add EXTERN and CALL to list of reserved keywords

e1555bd

draft version bump

c99bcda

macrologist mentioned this pull request Feb 21, 2024

Incorporate EXTERN and CALL RFC into spec #71

Closed

macrologist requested a review from stylewarning February 29, 2024 20:45

erichulburd approved these changes Mar 28, 2024

View reviewed changes

kalzoo reviewed Mar 28, 2024

View reviewed changes

Nits and typos

1e5d18d

macrologist merged commit 9748078 into quil-lang:master Apr 10, 2024

macrologist deleted the add-externs-to-spec branch April 10, 2024 15:18

erichulburd mentioned this pull request Aug 23, 2024

Support parsing of EXTERN / CALL instructions rigetti/quil-rs#393

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Include Extern specification #73

Include Extern specification #73

macrologist commented Feb 20, 2024 •

edited

Loading

erichulburd left a comment

erichulburd Mar 28, 2024

erichulburd Mar 28, 2024

erichulburd Mar 28, 2024

erichulburd Mar 28, 2024

kalzoo left a comment

kalzoo Mar 28, 2024

stylewarning Mar 30, 2024

kalzoo Mar 28, 2024

kalzoo Mar 28, 2024

kalzoo Mar 28, 2024

erichulburd Mar 29, 2024

kalzoo Mar 28, 2024 •

edited

Loading

erichulburd Mar 29, 2024

kalzoo Mar 28, 2024

macrologist Apr 1, 2024 •

edited

Loading

kalzoo Mar 28, 2024

kalzoo Mar 28, 2024 •

edited

Loading

macrologist Apr 1, 2024

erichulburd commented Mar 29, 2024

	PRAMGA EXTERN rng "INTEGER (seed : INTEGER)"
	PRAGMA EXTERN rng "INTEGER (seed : INTEGER)"

	PRAMGA EXTERN rng "(out : mut INTEGER, seed : INTEGER)"
	PRAGMA EXTERN rng "(out : mut INTEGER, seed : INTEGER)"

	restrictions: the extern MUST have a known function signature, which
	restrictions: the extern MUST have a declared function signature, which

Include Extern specification #73

Include Extern specification #73

Conversation

macrologist commented Feb 20, 2024 • edited Loading

erichulburd left a 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

kalzoo left a 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

kalzoo Mar 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

macrologist Apr 1, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kalzoo Mar 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erichulburd commented Mar 29, 2024

macrologist commented Feb 20, 2024 •

edited

Loading

kalzoo Mar 28, 2024 •

edited

Loading

macrologist Apr 1, 2024 •

edited

Loading

kalzoo Mar 28, 2024 •

edited

Loading