[WSL] WIP, some work on the spec.
authorrmorisset@apple.com <rmorisset@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Wed, 11 Jul 2018 17:29:31 +0000 (17:29 +0000)
committerrmorisset@apple.com <rmorisset@apple.com@268f45cc-cd09-0410-ab3c-d52691b4dbfc>
Wed, 11 Jul 2018 17:29:31 +0000 (17:29 +0000)
git-svn-id: https://svn.webkit.org/repository/webkit/trunk@233733 268f45cc-cd09-0410-ab3c-d52691b4dbfc

Tools/ChangeLog
Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott
Tools/WebGPUShadingLanguageRI/SpecWork/source/index.rst

index ff25903..fb1596e 100644 (file)
@@ -1,3 +1,16 @@
+2018-07-11  Robin Morisset  <rmorisset@apple.com>
+
+        [WSL] WIP, more of the spec
+        https://bugs.webkit.org/show_bug.cgi?id=186310
+
+        Rubberstamped by Filip Pizlo.
+
+        Fixed a few issues with the formal rules (such as adding the restrictions on pointers for compilation to SpirV),
+        and started writing some of the english in the spec.
+
+        * WebGPUShadingLanguageRI/SpecWork/WSL.ott:
+        * WebGPUShadingLanguageRI/SpecWork/source/index.rst:
+
 2018-07-10  Aakash Jain  <aakash_jain@apple.com>
 
         [ews-build] Add build step to UnApply patch
index e0eb42f..c1fe489 100644 (file)
@@ -28,6 +28,7 @@ s :: stmt_ ::= {{com statement}}
     | { blockAnnot s0 .. sn } :: :: block
     | e ; :: :: effectful_expr
     | tval x : sid ; :: :: resolved_vdecl {{com post-monomorphisation variable declaration}}
+    | tval x : sid = e ; :: :: resolved_init_vdecl {{com post-monomorphisation}}
     | Loop ( s , s' ) :: :: loop_construct {{com Special, only during execution}}
     | Cases ( s0 , .. , sn ) :: :: cases_construct {{com Special, only during execution}}
     | Join ( s ) :: :: join_construct {{com Special, only during execution}}
@@ -132,18 +133,18 @@ B :: behaviour_ ::= {{com statement behaviour}}
     | ( B ) :: :: parens
 
 b :: single_behaviour_ ::=
-    | Return t :: :: return
+    | Return tval :: :: return
     | Break :: :: break
     | Continue :: :: continue
     | Fallthrough :: :: fallthrough
     | Nothing :: :: Nothing
 
 t {{tex \tau}} :: type_ ::= {{com type}}
-    | LVal ( tval ) :: :: lval {{com left value}}
+    | LVal ( tval , addressSpace ) :: :: lval {{com left value}}
     | tval :: :: tval
 tval {{tex {\tau^{val} } }} :: type_value_ ::=
-    | Ptr ( tval ) :: :: ptr {{com pointer}}
-    | Ref ( tval ) :: :: array_ref {{com array reference}}
+    | Ptr ( tval , addressSpace ) :: :: ptr {{com pointer}}
+    | Ref ( tval , addressSpace ) :: :: array_ref {{com array reference}}
     | [ tval ] :: :: array {{com array}}
     | bool :: :: bool
     | uint32 :: :: uint32 {{tex \textbf{uint32} }}
@@ -154,7 +155,7 @@ tx {{tex {\tau^{syntax} } }} :: type_syntactic_ ::= {{com syntactic type}}
     | tx * addressSpace :: :: ptr
     | tx [] addressSpace :: :: array_ref 
     | tx [ i ] :: :: array_fixed_size
-addressSpace :: address_space_ ::=
+addressSpace, as :: address_space_ ::=
     | thread :: :: thread
     | threadgroup :: :: threadgroup
     | device :: :: device
@@ -214,6 +215,8 @@ formula :: formula_ ::=
     | G |- isIntegerOrEnum ( t ) :: :: is_integer
     | G |- sc0 .. scn fully covers t :: :: full_switch_coverage % TODO: make it explicit
     | s != s' :: :: stmt_not_eq {{tex [[s]] \neq [[s']]}}
+    | tval != tval' :: :: tval_not_eq {{tex [[tval]] \neq [[tval']]}}
+    | as != as' :: :: address_space_not_eq {{tex [[as]] \neq [[as']]}}
     | b in B :: :: behaviour_in {{tex [[b]] \in [[B]]}}
     | b not in B :: :: behaviour_not_in {{tex [[b]] \not\in [[B]]}}
     | G = G' :: :: typing_env_eq
@@ -324,11 +327,11 @@ G |- tx : tval :: :: syntax :: '' {{com Evaluating types}} {{tex [[G]] [[|-]] [[
 
     G |- tx : tval
     ---------------------------------------- :: ref
-    G |- tx [] addressSpace : Ref(tval)
+    G |- tx [] addressSpace : Ref(tval, addressSpace)
 
     G |- tx : tval
     --------------------------------------- :: ptr
-    G |- tx * addressSpace : Ptr(tval)
+    G |- tx * addressSpace : Ptr(tval, addressSpace)
 
 defns
 well_formed :: '' ::=
@@ -341,7 +344,7 @@ G |- well_formed ( td ) :: :: top_level :: '' by
     G |- well_formed(tx f<()>() {s0..sn})
 
     G |- tx0 : tval
-    G[x0 -> LVal(tval)] |- well_formed (tx f<()>(tx1 x1, .., txm xm) {s0..sn})
+    G[x0 -> LVal(tval, thread)] |- well_formed (tx f<()>(tx1 x1, .., txm xm) {s0..sn})
     -------------------------------------------------------------------- :: func_param
     G |- well_formed (tx f<()>(tx0 x0, tx1 x1, .., txm xm) {s0..sn})
 
@@ -367,22 +370,31 @@ G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}
     G |- e : bool
     G |- s : B
     G |- s' : B'
+    Return Ptr(tval, as) not in B
+    Return Ptr(tval, as) not in B'
+    Return Ref(tval, as) not in B
+    Return Ref(tval, as) not in B'
     ------------------------------ :: if
     G |- if (e) s else s' : B + B'
+    % The last 4 premises are useful for compiling to SpirV
 
     G |- e : bool
     G |- s : B
+    Return Ptr(tval, as) not in B
+    Return Ref(tval, as) not in B
     ---------------------------------------------------------- :: do_while
     G |- do s while (e); : (B \ {Break, Continue}) + {Nothing}
     % Note: we could make this rule a bit more precise in the cases where we know that s always return/trap/break.. but such a piece of code is almost certainly a bug.
 
-    G |- e : t
-    G |- isIntegerOrEnum(t)
-    G |- sc0: t /\ .. /\ G |- scn: t
-    G |- sc0 .. scn fully covers t
+    G |- e : tval
+    G |- isIntegerOrEnum(tval)
+    G |- sc0: tval /\ .. /\ G |- scn: tval
+    G |- sc0 .. scn fully covers tval
     G |- sblock0: B0 /\ .. /\ G |- sblockn: Bn
-    Nothing not in B0 /\ .. /\  Nothing not in Bn
     B = U B0 .. Bn
+    Nothing not in B
+    Return Ptr(tval, as) not in B
+    Return Ref(tval, as) not in B
     --------------------------------------------------------------------------- :: switch
     G |- switch (e) {sc0: sblock0 .. scn : sblockn } : B \ {Break, Fallthrough}
 
@@ -395,31 +407,41 @@ G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}
     --------------------------------- :: fallthrough
     G |- fallthrough; : {Fallthrough}
 
-    G |- e : t
-    --------------------------- :: return
-    G |- return e; : {Return t}
+    G |- e : tval
+    ------------------------------ :: return
+    G |- return e; : {Return tval}
 
     ----------------------------- :: return_void
     G |- return ; : {Return void}
 
-    ----------------------- :: trap
-    G |- trap; : {Return t}
+    -------------------------- :: trap
+    G |- trap; : {Return tval}
 
     ------------------- :: empty_block
     G |- {} : {Nothing}
 
     G[x -> Nothing] |- tx : tval
-    G[x -> LVal(tval)] |- {s0 .. sn} : B
+    tval != Ptr(tval', as)
+    G[x -> LVal(tval, thread)] |- {s0 .. sn} : B
     s0 != tx' x; /\../\ sn != tx' x;
-    --------------------------------- :: variable_decl
+    s0 != tx' x = e'; /\../\ sn != tx' x = e';
+    -------------------------------------------- :: variable_decl
     G |- {tx x; s0 .. sn} : B
     % Note: we remove x from the environment before reducing tx, to avoid a situation where x is required in the definition of tx, which gets rather weird with multiple declarations
     % (see email from 20/06/2018).
-    % Note: there is a minor ambiguity between this rule and the next two, but it is harmless as the next two rules both fail in the next step
+    % TODO: we can maybe put types in a different namespace instead.
     % if they are applied where s is a variable declaration.
-    % Note: the second premise prevents redeclaration of a variable in the same scope it was declared in.
+    % Note: the last two premises prevent redeclaration of a variable in the same scope it was declared in.
     % Implemented naively it takes O(n**2) to check, but can easily be optimized.
 
+    G[x -> Nothing] |- tx : tval
+    G[x -> LVal(tval, thread)] |- e : tval
+    G[x -> LVal(tval, thread)] |- {s0 .. sn} : B
+    s0 != tx' x; /\../\ sn != tx' x;
+    s0 != tx' x = e'; /\../\ sn != tx' x = e';
+    -------------------------------------------- :: variable_decl_init
+    G |- {tx x = e; s0 .. sn} : B
+
     G |- s : B
     ------------ :: trivial_block
     G |- {s} : B
@@ -427,24 +449,26 @@ G |- s : B :: :: typing_statement :: '' {{com Validating statements' behaviours}
     G |- s : B
     G |- {s1 .. sn} : B'
     n > 0
+    Fallthrough not in B
     Nothing in B
     -------------------------------------- :: block
     G |- {s s1 .. sn} : (B \ {Nothing}) + B'
     % Note: the last premise forbids trivially dead code. It is optional and could be removed with no consequences on the rest of the language.
+    % Note: the penultimate premise makes it a bit easier to compile to MSL, could be relaxed in future versions of the language.
 
     G |- e : t
     ------------------- :: expr
     G |- e; : {Nothing}
 
 defn
-G |- sc : t :: :: typing_switch_case :: '' by
+G |- sc : tval :: :: typing_switch_case :: '' by
 
-    G |- rval : t
-    --------------- :: case
-    G |- case rval : t
+    G |- rval : tval
+    --------------------- :: case
+    G |- case rval : tval
 
-    ---------------- :: default
-    G |- default : t
+    ------------------- :: default
+    G |- default : tval
 
 defn
 G |- sblock : B :: :: typing_switch_block :: '' by
@@ -455,11 +479,12 @@ G |- sblock : B :: :: typing_switch_block :: '' by
 
 defn
 G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
-    ------------------- :: null_lit_array_ref
-    G |- null : Ref (tval)
 
-    ------------------- :: null_lit_ptr
-    G |- null : Ptr (tval)
+    -------------------------- :: null_lit_array_ref
+    G |- null : Ref (tval, as)
+
+    -------------------------- :: null_lit_ptr
+    G |- null : Ptr (tval, as)
 
     ---------------- :: literal_true
     G |- true : bool
@@ -496,42 +521,43 @@ G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
     -------------- :: not
     G |- !e : bool
 
-    G |- e : LVal(tval)
+    G |- e : LVal(tval, as)
     G |- e' : tval
-    ----------------- :: assignment
+    as != constant
+    ----------------------- :: assignment
     G |- e = e' : tval
 
     x -> t in G
     ----------- :: variable_name
     G |- x : t
 
-    G |- e : LVal(tval)
-    ---------------- :: lval_access
+    G |- e : LVal(tval, as)
+    ----------------------- :: lval_access
     G |- e : tval
 
-    G |- e : LVal(tval)
-    ---------------- :: address_taking
-    G |- &e : Ptr(tval)
+    G |- e : LVal(tval, as)
+    ----------------------- :: address_taking
+    G |- &e : Ptr(tval, as)
     % can the unary operator & be overloaded?
     % It seems that no
 
-    G |- e : Ptr(tval)
-    ----------------- :: ptr_deref
-    G |- *e : LVal(tval)
+    G |- e : Ptr(tval, as)
+    ------------------------ :: ptr_deref
+    G |- *e : LVal(tval, as)
     % can the unary operator * be overloaded?
     % It seems that no
 
     % Note: We currently do not have any special interaction between pointers and array references in these rules
     
-    G |- e : LVal(tval)
-    ---------------- :: take_ref_lval
-    G |- @e : Ref(tval)
+    G |- e : LVal(tval, as)
+    ------------------------ :: take_ref_lval
+    G |- @e : Ref(tval, as)
     % Note: in the execution rules, the behaviour depends on whether that LVal points to an array, but here we don't need to track it.
 
-    G |- e : LVal([tval])
+    G |- e : LVal([tval], as)
     G |- e' : uint32
-    -------------------- :: array_index_lval
-    G |- e[e'] : LVal(tval)
+    --------------------------- :: array_index_lval
+    G |- e[e'] : LVal(tval, as)
 
     G |- e : [tval]
     G |- e' : uint32
@@ -542,10 +568,10 @@ G |- e : t :: :: typing_expr :: '' {{com Typing expressions}} by
     % TODO: should we refuse during validation the case where e' is a constant that falls out of the bounds of e ?
     % I think it should be an allowed behaviour but not required of the implementation.
 
-    G |- e : Ref(tval)
+    G |- e : Ref(tval, as)
     G |- e' : uint32
-    -------------------- :: array_ref_index
-    G |- e[e'] : LVal(tval)
+    --------------------------- :: array_ref_index
+    G |- e[e'] : LVal(tval, as)
 
     G |- e0 : tval0 /\../\ G |- en : tvaln
     x -> Func{sig0, .., sigk} in G
@@ -726,6 +752,14 @@ R |- s -> s' ; E ; S :: :: exec_stmt :: '' {{com Small-step reduction on stateme
     ------------------------------------------------------------ :: block_vdecl
     Rout |- {R tval x : sid; s1..sn} -> {R' s1..sn} ; sid <- rv;
 
+    R[x -> LVal(sid)] |- e -> e';;
+    ------------------------------------------------------------ :: block_vdecl_init_reduce
+    Rout |- {R tval x : sid = e; s1..sn} -> {R tval x : sid = e'; s1..sn} ;;
+
+    R' = R[x -> LVal(sid)]
+    ------------------------------------------------------------ :: block_vdecl_init_complete
+    Rout |- {R tval x : sid = rv; s1..sn} -> {R' s1..sn} ; sid <- rv;
+
     R |- e -> e' ; E ; S
     ---------------------- :: effectful_expr_reduce
     R |- e; -> e'; ; E ; S
index 2bd8eb7..12922a8 100644 (file)
@@ -64,6 +64,8 @@ The following strings are reserved keywords of the language:
 | Reserved for future extension | protocol auto                                                                   |
 +-------------------------------+---------------------------------------------------------------------------------+
 
+``null``, ``true`` and ``false`` are keywords, but they are considered literals in the grammar rules later.
+
 Similarily, the following elements of punctuation are valid tokens:
 
 +----------------------+-----------------------------------------------------------------------------------------------+
@@ -193,8 +195,7 @@ Then, we apply the following two rules:
 
 Complex variable declarations are also mere syntactic sugar.
 Several variable declarations separated by commas are the same as separating them with semicolons and repeating the type for each one.
-And a variable declaration with an initializer is the same as an uninitialized declaration, followed by an assignment of the corresponding value to this variable.
-These two transformations can always be done because variable declarations are only allowed inside blocks (and for loops, but these get desugared into a block, see above).
+This transformation can always be done because variable declarations are only allowed inside blocks (and for loops, but these get desugared into a block, see above).
 
 .. todo:: should I make the requirement that variableDecls only appear in blocks be part of the syntax, or should it just be part of the validation rules?
 
@@ -274,8 +275,8 @@ it can be done just by wrapping the expression in parentheses (see the last alte
 .. productionlist::
     constexpr: `Literal` | `Identifier` "." `Identifier`
 
-Static rules
-============
+Validation
+===========
 
 Phase 1: Gathering declarations
 -------------------------------
@@ -306,7 +307,7 @@ Typedefs and structs:
 
 Structs:
 
-- checking that structs have distinct names for different fields, and that the type of their fields are well-defined
+- checking that structs have distinct names for different fields, and that the type of their fields are well-defined (and non-void)
 
 Enums:
 
@@ -325,6 +326,7 @@ Functions:
 - check that operator.field= is only defined if operator.field is as well, and that they agree on their return type in that case.
 - check that operator[]= is only defined if operator[] is as well, and that they agree on their return type in that case.
 - check that all of the type parameters of each operator declaration/definition are inferrable from their arguments (and from its return type in the case of cast operators).
+- check that no argument is of type void
 - finally, check that the function body can only end with a return of the right type, or with Nothing if it is a void function
 
 Typing statements
@@ -337,6 +339,7 @@ Typing expressions
 - checking returns
 - check that every variable declaration is in a block or at the top-level
 - check that no variable declaration shadows another one at the same scope
+- check that no variable is declared of type void
 - check that switch statements treat all cases
 - check that every case in a switch statement ends in a terminator (fallthrough/break/return/continue/trap)
 - check that literals fit into the type they are stored into (optional?)
@@ -357,9 +360,89 @@ Dynamic rules
 Definitions
 -----------
 
+We split the semantics in two parts: a per-thread execution semantics that does not know anything about concurrency or the memory, and a global set of rules for
+loads, stores, barriers and the like.
+
+The per-thread semantics is a fairly classic small-step operational semantics, meaning that it describes what a list of possible transitions that the program can
+take in one step.
+The per-thread state is made of a few element:
+
+- The program being executed. Each transition transforms it.
+- A control-flow stack. This is a stack of values, which tracks whether we are in a branch, and is used by the rules for barriers to check that control-flow is uniform.
+- A (constant) environment. This is a mapping from variable names to values and is used to keep track of arguments and variables declared in the function.
+
+Each transition is a statement of the form "With environment :math:`\rho`, if some conditions are respected, the program may be transformed into the following, modifing
+the control-flow stack in the following way, and emitting the following memory events."
+
 Execution of statements
 -----------------------
 
+Blocks and variable declarations
+""""""""""""""""""""""""""""""""
+
+The program fragments that we use to define our semantics are richer than just the syntactically correct programs. In particular, we allow annotating blocks
+(sequences of statements between braces) with an environment.
+
+Here is how to reduce a block by one step:
+
+#. If the block is not annotated, annotate it with the environment
+#. If the first statement of the block is an empty block, remove it
+#. Else if the first statement of the block is a terminator (break, continue, fallthrough, return or trap), replace the entire block by it.
+#. Else if the first statement of the block is a variable declaration:
+
+   #. Make a new environment from the one that annotates the block, mapping the variable name to its store identifier.
+   #. If the variable declaration has an initializing expression that can be reduced, reduce it using the new environment
+   #. Else:
+
+      #. Change the annotation of the block to the new environment.
+      #. Emit a store to the store identifier of the declaration, of a value that is either the initializing value (if available) or the default value for the type (otherwise)
+      #. Remove this variable declaration from the block
+
+#. Else reduce the first statement of the block, using the environment that the block was annotated with (not the top-level environment)
+
+.. todo:: Specify this "default value for the type". It should be very simple (null for ptrs/refs, false for booleans, 0/0. for ints/floats, and the natural extension for arrays/structs).
+
+Branches
+""""""""
+
+We add another kind of statement: the ``Join(s)`` construct, that takes as argument another statement ``s``.
+
+Here is how to reduce a branch (if-then-else construct, remember that if-then is just syntactic sugar that was eliminated during parsing) by one step:
+
+#. If the expression in the if is ``true`` or ``false``.
+
+   #. Push that value on the control flow stack
+   #. Replace the branch by the statement in the then (for ``true``) or else (for ``false``) branch, wrapped in the ``Join`` construct
+
+#. Else reduce that expression
+
+Here is how to reduce a ``Join(s)`` statement:
+
+#. If the argument of the ``Join`` is a terminator (``break;``, ``continue;``, ``fallthrough;``, ``return e?;`` or ``trap;``) or an empty block
+
+   #. Pop the last value from the control flow stack
+   #. Replace the ``Join`` statement by its argument
+
+#. Else reduce its argument
+
+.. note:: Popping the last value from the control flow stack never fails, as a Join only appears when eliminating a branch, which pushes a value on it.
+
+Switches
+""""""""
+
+We add another kind of statement: the ``Cases(..)`` construct that takes as argument a sequence.
+
+Loops
+"""""
+
+Barriers and uniform control flow
+"""""""""""""""""""""""""""""""""
+
+Other
+"""""
+
+TODO: return reduce, and effectful expr.
+
 Execution of expressions
 ------------------------