Re: The design of WebAssembly

Hi David,

Sorry for the long delay.  I’ve been busy.

CCured: https://www.cs.virginia.edu/~weimer/p/p477-necula.pdf
Cyclone: http://cyclone.thelanguage.org/wiki/Papers/

The Cyclone typesystem is among my favorites.  We could use something much simpler, since Cyclone was so concerned with object lifetimes.  We don’t have that problem.

Someone asked if we could statically prove that all accesses are in bounds.  This kind of thing is possible.  For example: https://en.wikipedia.org/wiki/SPARK_(programming_language)

Unfortunately, the techniques used to make this work make programming very cumbersome.  Getting a seemingly obviously correct program to typecheck can be hard because the type system is basically a proof assistant at that point.  So, I don’t think it’s a very scalable approach.

-Filip


> On Aug 25, 2017, at 2:43 PM, David Neto <dneto@google.com> wrote:
> 
> Thanks for these references.  I've read through the Semantics.md and the Rationale.md and have just started the PLDI paper.
> 
> WebAssembly looks well thought-out.  A couple of initial thoughts:
> - You're trying to support more capable programs than traditionally run on GPU.   That's fair given that it's supposed to support "main thread" kinds of apps.
> - The docs talk about how nondeterminism will creep in once threads are supported.  It's good to acknowledge.  This is a big issue: concurrency is pervasive in GPU shaders.  :-)
> - WebAssembly supports recursion, so it uses a general purpose stack to support it.  That motivates a lot of the design, and parts of the soundness proofs.
>   Shader languages typically ban recursion, so no general stack is required. That simplifies a lot.
> - WebAssembly supports indirect calls (e.g. function pointers). 
>   Shader languages I know of ban function pointers.  Again, this simplifies a lot.
> - For safety, WebAssembly segregates various things like local variables, code, tables, and general purpose memory (memories).   A reference to one thing can't accidentally alias to a reference to another.   I'll have to write down the argument for it, but SPIR-V with Logical Addressing is intended to provide veriy similar separate-by-construction guarantees.
> 
> 
> While I'm at it:    Fil: Please post those URLs to the work you cited.
> 
> 
> Thanks
> david
> 
> 
> On Thu, Aug 24, 2017 at 12:31 AM JF Bastien <w3c@jfbastien.com <mailto:w3c@jfbastien.com>> wrote:
> In the call today Ken asked about what other projects had tackled problems similar to what WebGPU is trying to do, and asked folks to provide references.
> 
> Here's a paper a few of us wrote about WebAssembly:
> https://github.com/WebAssembly/spec/blob/master/papers/pldi2017.pdf <https://github.com/WebAssembly/spec/blob/master/papers/pldi2017.pdf>
> 
> Of course it's not all relevant to WebGPU, but it's a good starting point to try to break down how we approached the design space, and what considerations were taken. I'm happy to answer any questions this raises.
> 
> There's also a non-comprehensive rationale document:
> https://github.com/WebAssembly/design/blob/master/Rationale.md <https://github.com/WebAssembly/design/blob/master/Rationale.md>
> It would be cool if WebGPU did a better job that WebAssembly and kept better documentation.
> 
> Fil said he'd provide references for other projects too, I'll let him do that :)