Where should the memory model spec live?

[littledan]

Three options:

• Wasm spec references JS spec for the memory model. This is the easiest model to start with. If Wasm needs to express something that's not available in JS, it can explain that in terms of a patch to the JS memory model. We can refactor the JS memory model to make it more amenable to use by Wasm, if it makes sense.
• Separate JS and Wasm memory models. This avoids the Wasm spec normatively referencing the JS spec, wihch @rossberg-chromium considered a goal. However, considering that they may be operating on the same block of memory, it could become a bit difficult to understand what guarantees there are when the worlds interact.
• Wasm spec and JS spec both reference an underlying separate memory model spec. Possibly best of both worlds? There are just some organizational boundaries. We also may have some iteration on the format, if some feel that the JS memory model isn't using the right kind of notation/formalism (could be a pro or con).

Any thoughts on these options?

(thread split off from https://github.com/WebAssembly/threads/issues/9)

[lars-t-hansen]

Whatever we do here, somebody is going to end up with the short end of the stick. Option 1 is bad for wasm because it makes wasm beholden to JS in a way we don't want to be. Option 2 is bad for interop with the web stack (actually with anything at all unless the wasm model is tied to some other stack specifically here). Option 3 is bad for interop with other technology stacks than the web.

Option 3 has been generally assumed in discussions I've been involved in, both in TC39 and elsewhere. And it has the nice feature that there can be more than one of these: there can be a wasm-and-JS spec, and if there are other technology stacks (call them X) where wasm figures prominently there can perhaps be a different wasm-and-X spec. Both wasm-and-JS and wasm-and-X will be constrained by the needs of wasm, but it's likely manageable.

[rossberg]

These are fair questions, but for now they are putting the cart three kilometers before the horse. There is a lot to be resolved first. This is a much more complex discussion than a GitHub issue can swallow, but let me note just a few things.

Weak memory models are a very, very hard problem, probably the hardest in language semantics so far. There has been more than a decade of research leading to the current C++ and Java models and they still have fundamental flaws. Defining a memory model for a language is not merely a matter of calling into some operations, it is intimately intertwined with the entire language, and requires a holistic definition.

As far as I am aware, nobody has ever tackled a multi-language weak memory model. Such a setting makes an already difficult problem combinatorially harder, and is a completely open research problem. Developing a meaningful and practically feasible approach to this will probably be worth several PhDs on the way.

We should not pretend that we have a solution to this problem. Sure, we could write up something nicely sounding that is "shared" between the two documents (in whatever place). But that would just create an illusion. Technically, it would be completely void unless we actually know what we are doing. And a meaningless semantics is not going to help anybody on either end and provides no guarantees whatsoever.

A sensible order of attacking this problem is to first figure out a semantics for either language (hard enough!) and build sufficient confidence that they actually do what we think they do. Then we could start thinking about ways to integrate those into some unified model. Everything else is just pretending, and no more useful than putting in an informal note saying that we assume these languages interoperate as expected.

The good news is that there already are expert researchers starting to tackle the first part of the problem.

[littledan]

@lars-t-hansen For Option 1, is there more I could read about the goals of Wasm being independent from JS? Is this about JS object semantics accidentally creeping in, or because of difficulties in working with TC39, or something else?

For Option 3, I don't quite understand how it would be bad for technology stacks other than the web. If JS doesn't depend on the web, and Wasm doesn't either, why would their shared memory model doc depend on it?

@lars-t-hansen @rossberg-chromium For Option 2, Is anyone considering a threaded Wasm where the memory isn't made accessible to JavaScript? That seems like the world that would be bad for interoperability. If the memory will be available to JavaScript, then it's just a decision to not try to formalize the full memory model. That could be fine--it's not like Java waited to have a standardized memory model before shipping threads.

The reason I'm putting the cart before the horse on where we do the memory model before we even have this work all done is because there's a bit of organizational work and lead time to choosing a standards venue, getting everyone to agree on it and reference the document produced, IP issues, boring things like that, that are independent of the actual content. If it's a third document, we should also be prepared to have differences in notation and some kind of "binding" to describe how they interact (since Wasm elected not to use JS's notation, there'll be at least one mismatch).

[rossberg]

@littledan, we are considering Wasm implementations with no JavaScipt whatsoever. Some people have already started building them. Enabling that was an explicit design goal from the beginning, and the reason why we carefully layered design and specs to avoid spurious dependencies.

[littledan]

I guess I meant to ask more specifically, is anyone considering that for the web embedding, threads might not give an option to share the memory with JavaScript? (There's a there-exists vs for-all difference here...)

[rossberg]

@littledan, not sure if that's what you're asking, but a Wasm module can always choose to keep its memory private. In that case, JS has no way of accessing it. So sharing is not required, but of course it is meant to be possible on the web.

[lukewagner]

@rossberg-chromium What you're describing makes sense if we want to convert everything over to an operational memory semantics. This is something I'd love and hope we eventually do; it seems like bleeding-edge research though and it'll take a long time though.

In the short-term, I think there is a hybrid approach that still keeps the core wasm spec JS-agnostic by making the necessary interactions points with the JS memory model go through host-environment-defined hooks (kinda like how we do with JS imports).

More specifically, it looks like when you, e.g., execute SetValueInBuffer in JS on a SAB, you semantically append a WriteSharedMemory event to some [[EventList]]. To plug into this from wasm, it seems like we just need the core semantics of store et al to call a host-environment-defined function, passing the requisite data, so that the JS+Web binding spec can then go append a WriteSharedMemory event etc etc.

If we did that, then:

1. from a JS POV, we could consider wasm just to be host builtins that are semantically called by the JS spec and emit shared memory events that participate in the overall JS memory model.
2. from a wasm POV, we've bought time to attack the hard problems about how to do an operational memory model because, in the meantime, on the Web, JS+wasm shmem is no less well defined than JS shmem b/c of point 1.

[rossberg]

@lukewagner, unfortunately, there are several problems with that. For example:

• From the Wasm side, you can only model something as a "call" to an abstract operation if it is an atomic action. There is no way to specify the possible interleavings of an abstract call with other Wasm threads. For example, tearing memory accesses cannot be modelled that way. (This problem extends to host function calls, btw. -- or the inverse, for that matter.)

• I have no idea how to share/extend e.g. the definition of execution sets across separate languages -- which would be the whole point of a shared semantics. Just sharing abstract operators is useless on its own.

• In general, nobody seems to know how to properly hook up an axiomatic memory model with an operational semantics -- not even the experts. It is unclear how to superimpose something like the notion of valid execution set on a standard reduction relation. I suppose it could be done with a nondeterministic labelled transition system somehow, but AFAICT that is not something that is common practice.

FWIW, multi-language semantics is an ongoing research problem on its own, even without weak memory making everything harder. That is regardless of the specification method. I'm highly skeptical that we would be able to come up with anything meaningful. Or that it is energy well-spent to try.

[jfbastien]

@rossberg-chromium

nobody seems to know how to properly hook up an axiomatic memory model with an operational semantics

Do we need to?

multi-language semantics

Is that what we want to be defining as the memory model? Or do we want to be defining a virtual ISA, the same way x86, ARM, POWER, NVIDIA hardware, all have an ISA memory model independent of the languages that execute on them. In that approach it's up to each language to figure out how it maps to the shared model.

It seems to me that we can define the WebAssembly virtual ISA's memory model, and (as you say) handwave the mapping for a while, let the PhDs mint themselves. I think we'll still have something that extremely practical and useful albeit not Mathematically Pure And Satisfying.

[rossberg]

@jfbastien

nobody seems to know how to properly hook up an axiomatic memory model with an operational semantics

Do we need to?

If you don't relate it to execution, then what does it mean?

multi-language semantics

Is that what we want to be defining as the memory model? Or do we want to be defining a virtual ISA, the same way x86, ARM, POWER, NVIDIA hardware, all have an ISA memory model independent of the languages that execute on them. In that approach it's up to each language to figure out how it maps to the shared model.

That's a different scenario. We are not compiling one language into the other. We have two languages with different concepts that interact with each other directly. There is no common low-level execution model that underlies both.

It seems to me that we can define the WebAssembly virtual ISA's memory

model, and (as you say) handwave the mapping for a while, let the PhDs mint themselves. I think we'll still have something that extremely practical and useful albeit not Mathematically Pure And Satisfying.

Well, all these memory models are fairly mathematical in nature. As such, they either make sense or they don't. They can also model the wrong thing, but other than that there isn't much middle ground.

[jfbastien]

Let's try to break this down...

Do you agree that we can separately spec the WebAssembly virtual ISA's memory model? Not whether we should, but whether it is possible?

IIUC your point is that if we take this approach, then the mapping of each language to that virtual ISA's model is still imprecise. Correct?

Can you describe the alternate approach, where we don't do this? It seems to me like we'd be in a yet more imprecise world for longer still, without any model at all, while we wait for academia to solve a very hard problem. That seems less desirable, but you seem to think otherwise. Can you explain why?

[lukewagner]

@rossberg-chromium

From the Wasm side, you can only model something as a "call" to an abstract operation if it is an atomic action.

IIUC, the "atomic action" is inserting a memory event (read, write, rmw) into the [[EventList]].

I have no idea how to share/extend e.g. the definition of execution sets across separate languages -- which would be the whole point of a shared semantics.

What I'm suggesting above is that, until we arrive at something better, we could start by not trying to solve this problem in the core wasm spec but rather just calling "hooks" and it's only when you take JS+wasm together (or X+wasm for non-Web) that you can talk about a memory model. This is symmetric to what we've done with using workers as threads. And just like we can later pull threads "into" wasm (viz pure wasm threads), we could also pull in the memory model later (probably we'd even need to do the two at the same time).

[littledan]

To be a little more concrete about a refactoring that could make sense to support Wasm more cleanly: Currently, functions like SetValueInBuffer operate on JS values like Number (and BigInt in the possible future) and type names based on TypedArrays. A Wasm binding here would have to go and fake creating those JS values. The memory model can instead talk explicitly about values of particular non-JS types for actual 32-bit and 64-bit floats and ints, and have JS convert into them. This requires a little more wording for JS to hook up to it, and has the benefit that Wasm wouldn't have to create any sort of values that don't make sense in the Wasm context.

Well, all these memory models are fairly mathematical in nature. As such, they either make sense or they don't. They can also model the wrong thing, but other than that there isn't much middle ground.

@rossberg-chromium Would a memory model be entirely useless if a bug is found in it later? It happens pretty frequently that there are bugs in specs which implementations don't implement, and the world doesn't fall apart. Then the bug gets found and fixed, and everything's OK. I don't think implementations are going to be saying, "Wow, I can derive false from these axioms, so I'll do whatever I want!"

[rossberg]

This discussion is focused on memory operations, but they are not what actually matters much in a memory model! The crux of a memory model is the specification of possible execution orders between uses of these operations, which is a completely non-obvious problem. Without that there isn't much point in meddling with abstract operations, they are trivial on their own (especially the atomic ones!).

So, the primary problem is not that we introduce bugs (although I'm sure we gonna do that, too). It is that the "specification" will not actually specify anything of interest. Or worse, specifies the completely wrong thing. And that's independent of how "mathematical" it is.

And yes, to answer @jfbastien's question, that is worse than the alternatives!

• If we keep the specs separate then we at least have a feasible chance of saying something reasonable about the memory model of each language individually. On top of that we can add (for the time being) some handwaving pointing out that these models are intended to be compatible and expected to interact in the "obvious" manner.

• If, on the other hand, we prematurely try to share something that is basically meaningless, then we'll not just have failed to specify interop, we also will have failed to specify the individual languages themselves. That is a strictly worse outcome.

So I suggest not making naive attempts to solve a hard problem that nobody has solved before (and introduce needless complexity and bureaucracy on the way). Instead, stick to what we have a reasonable chance of getting right, and leave the rest for future research to figure out.

@lukewagner, I don't think we can avoid talking about threads in the Wasm spec either. They exist and have observable semantics, regardless of how they are created (to make an analogy with functions: for now we just have "host threads"). But I believe they are fairly easy to incorporate and hook up.

[lukewagner]

@rossberg-chromium The JS spec specifies possible execution orders, no? So if, from a purely JS POV, the core wasm spec is just defining host builtins that can be called by JS and that emit the same memory ordering events in the same agents as JS and thus participate in computing the valid candidate executions, that seems no less well-defined than JS currently is. Right?

Of course this means that you can't reason about wasm+threads in isolation, without pulling in some host specification, and I think that is your main point of contention, but my point is that this could be a temporary stage while we work out the more challenging questions of how to do it within wasm in a way that interops with JS. MVP and all that.

[rossberg]

@lukewagner, yes, and the definition of candidate executions relies on agents, which "comprise a set of ECMAScript execution contexts, an execution context stack, a running execution context" etc. All of that only makes sense for JavaScript (besides being rather handwavy). For WebAssembly, completely different definitions would be needed to give it meaning, and nobody knows how. And it's even less clear how to define all that in such a way that uncouples it from the individual language specs, because it interacts with all their execution rules.

[jfbastien]

@rossberg-chromium so you're satisfied with the definition of possible execution orders (not all the details, just its general existence), but not with the definition of agents?

[rossberg]

@jfbastien, well, without a suitable Wasm definition of agent that connects it to Wasm execution the definition of execution order is totally vacuous. It wouldn't specify anything about the behaviour of Wasm (nor Wasm+JS). Problem is, nobody knows how to make such a connection, let alone how to make it work properly across multiple language semantics.

[jfbastien]

I don't understand why you think this is the case. Defining possible execution orders is the harder part in my understanding, because the other agents we're talking about aren't exotic agents which operate weakly through any of SIMD, different processes, different non-coherent hardware, or different machines. We're only adding same-process agents, those are fairly straightforward in my understanding.

Do you have data stating otherwise? I may have misses something in the literature and would like to catch up if that's the case.

[syg]

nobody seems to know how to properly hook up an axiomatic memory model with an operational semantics

@rossberg-chromium Are you contending that the 2-stage "filtering" semantics in ECMAScript doesn't work correctly? Or is the point that you'd like an operational semantics to compute possible values at "step time", without the computationally intractable thing of considering the universe of all possible candidate reduction traces?

I also am confused by why using the ECMAScript axiomatic model as a "filter" on possible reduction traces means it cannot say anything about Wasm. I have more worries about the other way: proving some notion of behavioral equivalence or refinement between two independent weak memory models with different machinery. I have no mental model of how I'm supposed to reason about an SAB shared between browser JS and wasm if there is no common ground somewhere.

[rossberg]

@syg, I see a number of issues and mismatches between the two languages. For example, off the top of my head:

• The definition of "agent" (as well as execution context), which the notion of execution depends on, is completely different. You can try to take an "additive" approach to defining an agent's state, but I still have no idea how you would describe the actual interaction between the two languages, i.e., Wasm calls that are nested into JS execution and vice versa, where execution contexts would have to compose somehow.

• The Ecma spec is not declarative but "algorithmic" and imperative: in particular, events are created and appended to a list; modifications to this list are described by spec-internal global mutable state (and there is quite a bit of hand-waving involved in interpreting how the non-determinism interacts with that, how the axiomatic rules restrict it, and how threads are interleaved in general). That does not mesh well with the standard text book model used in Wasm, which is based on a more precise declarative reduction semantics.

• The standard way of attaching events to a reduction relation is through labeled transitions. The labels would be the event lists. In analogy with the Ecma memory model you could then impose a similar axiom system to restrict the allowed event sequences. However, this may or may not be the best way to do it. Do you have any reference where such a combination has already been used successfully to specify a weak memory model? Or a viable alternative?

• The "bulk" nature of the memory events currently defined in Ecma is at odds with a precise semantics. A reduction relation has to allow all possible interleavings, otherwise the axiomatic "filtering" you mention isn't really possible. In particular, any read or write that is not atomic, and thus e.g. allows tearing to be observed, would have to be split into multiple steps. Consequently, I imagine the memory events would need to be split up accordingly (on both sides!). (Which may, in fact, simplify the definition of reads-from.)

• Wasm will eventually have other events than just access to linear memory. For example, module instantiation or shared globals, which have to be incorporated into the memory model. There may be things that won't arise on the JS side, and vice versa. Generally, the set of events is highly language-specific, and I suspect that any premature attempt to define one abstract model to rule them all is gonna be cumbersome or incomplete or both, and cause trouble down the road.

• Most importantly, even if we managed to resolve all that, I expect that any attempt of factoring the definitions of agents, execution contexts, memory events, etc will almost inevitably end up being specific to a JS embedding. That would de facto tie Wasm to JavaScript, with no way to specify other embeddings.

As mentioned before, both weak memory models and multi-language semantics are already very hard problems in isolation. And @jfbastien, I am not aware of any successful attempt to day that solved both together in a meaningful manner (but I'm happy to be proven wrong!).

I am somewhat optimistic that most of this can be solved eventually, but honestly, I think we are years away from a proper solution. Rushing something incoherent won't help anybody either -- @syg, how would you reason about the SAB interaction when its specification is not meaningful? That has no more value than informal statements of intent, and creates more problems than it solves, both technically and administratively.

[rossberg]

PS: For the experts, the primary mismatch probably boils down to ES defining (essentially) a big-step semantics, while Wasm is using a small-step semantics. The problem with big-step is that it provides no clean way to specify threading, which is why the entire concurrency story in the ES spec really is a big hand-wave. For Wasm we wanted to avoid that, which is why we switched to small-step. Unfortunately, it is quite difficult to model an interaction between the two approaches, even for trivial toy systems (an extension of the problem that big-step has with threads already).

[littledan]

@rossberg-chromium The first two problems need to be solved in formalizing the JS.md specification, which exactly is supposed to hook up Wasm's formalization with JS for single-threaded code. There's some JS specific parts, but there are other parts that are just about, "actually do this thing in the Wasm spec", which is a bit awkward to word. The latter category isn't really specific to a connection to JS at all; if you were documenting how Wasm executes in any other context, I think at some point you'd have to say, "parse the binary format into an AST, then execute it until it's done executing. And if Wasm calls out into a native function, run it, and run any Wasm callbacks that the native function invokes". If any connection between small-step semantics and imperative descriptions of what actually might happen is hand-wavy by your standards, then we're just going to have to have a somewhat hand-wavy specification. The alternative would be a formalism floating in the air and no documented way to invoke it.

(Is there any sort of bug thread or discussion notes from when the current formalism was chosen? I don't really understand how the Wasm spec is more precise than the JS one (ignoring the areas where the JS spec is deliberately imprecise).)

[syg]

Andreas, Luke, and I discussed near(er)-term plans for the wasm memory model, focusing on interop with the JS embedding. Please correct me if I incorrectly sum up anything here.

The nearer term plan would be to try to factor out a common core event semantics and the weakest-possible-yet-still-meaningful set of constraints. Instead of this core event semantics be normatively referenced by both JS and wasm, the normative versions for both specs will remain inlined, so as to reduce friction for moving forward. There will then be a non-normative note (Andreas suggested the best place would be the JS-wasm bridge spec) with concise math that serves as the intended semantics that both JS and wasm are supposed to be observationally equivalent to.

I'm not sure how this should be best spun -- the intent needs to communicate that if the event semantics diverge between JS and wasm, that is a spec bug in one, or both. This is not quite the teeth that "non-normative" has. What do folks think is the best approach here? Perhaps Dan can chime in.

On the academic research front, Peter's work has been great and it'd be awesome if he looks into this. I think it is very important that he collaborates with the work that Clark and Cristian has already done. There's no current plans with Peter's group AFAIK, however.

I'll be happy to float the idea of this style of factoring to TC39 once details are more concrete on the wasm side.

[rossberg]

@syg summed it up nicely. Here are some additional details of our discussion (@syg and @lukewagner correct me if I'm wrong).

There are two properties of the Wasm core spec that we want to maintain:

1. It should remain independent of a specific embedder/language, and not privilege one.
2. It should remain meaningful even without an embedder spec.

The goal for the memory model hence is to

• make it generic enough that it can support different host languages,
• but make it customisable through some suitable parameterisation.

Details to be worked out. The basic idea is that the Wasm spec will contain a "minimum" memory model, but embedder specs (such as the JS API) can refine and extend it with additional host events and ordering constraints. For now, an axiomatic formulation seems like the easiest way to get there. I will look into ways of integrating that with the Wasm spec.

Obviously, it is not clear what a sufficiently "generic" model really is or how different spec approaches to semantics could be reconciled for other languages. So despite the first goal above, the initial model will naturally be informed primarily by the needs of JS. But at least we want to avoid knowingly introducing dependencies. We expect that the model will evolve if other embedder specs pop up or research on memory models offers new insights.

Moreover, we discussed how to implement sharing between the Wasm and the ES spec. It seems like the amount of definitions that would actually be common to both specs is not really large enough to motivate yet another spec (especially if kept non-JS-specific). It would create tedious indirection and extra churn, and may complicate adapting to new Wasm embedders. As Shu mentioned, we arrived at the idea of rather including the respective pieces in both specs, and then describe the unified semantics in the JS API spec that bridges the two.

[littledan]

Being independent of various things sounds like a great goal for keeping these specs clear, meaningful and capable of evolving into the future. If there's sufficient non-normative text that can explain what's supposed to going on to normal implementers and users, this could be a working solution for everyone.

However, there's another goal which is (unfortunately) in tension with this independence. That goal is having the combination of all of the specifications completely describe the system, to the point that could, in theory, read all the specs in the world and write a web browser that can run the whole web. In several other areas of the web platform, ideas about definitions being clean and independent of other things has gotten in the way of being complete enough (it would be too messy to specify that part!), or has made their evolution over time difficult (e.g., in adding features that integrate with other parts which breaks the abstraction boundaries). Sometimes, abstraction boundaries turn out to be in the wrong place when attempting to actually take advantage of the generic-ness.

I hope, as the Wasm specification evolves here, we can keep in mind the balance between good abstractions and complete, web-ready descriptions.

[syg]

That's a good goal, but the reality of memory models is that no implementer will read the actual memory model for implementation guidance. They will read the non normative guidelines or will lean on experts. As far as the MM goes, then, I think the outlined approach doesn't run counter to this goal in practice.

-- shu

On Sep 18, 2017, at 09:05, Daniel Ehrenberg notifications@github.com wrote:

Being independent of various things sounds like a great goal for keeping these specs clear, meaningful and capable of evolving into the future. If there's sufficient non-normative text that can explain what's supposed to going on to normal implementers and users, this could be a working solution for everyone.

However, there's another goal which is (unfortunately) in tension with this independence. That goal is having the combination of all of the specifications completely describe the system, to the point that could, in theory, read all the specs in the world and write a web browser that can run the whole web. In several other areas of the web platform, ideas about definitions being clean and independent of other things has gotten in the way of being complete enough (it would be too messy to specify that part!), or has made their evolution over time difficult (e.g., in adding features that integrate with other parts which breaks the abstraction boundaries). Sometimes, abstraction boundaries turn out to be in the wrong place when attempting to actually take advantage of the generic-ness.

I hope, as the Wasm specification evolves here, we can keep in mind the balance between good abstractions and complete, web-ready descriptions.

― You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.