- Where: zoom.us
- When: April 16, 4pm-5pm UTC (April 16, 9am-10am Pacific Daylight Time)
- Location: link on calendar invite
- Contact:
- Name: Ben Smith
- Email: [email protected]
None required if you've attended before. Email Ben Smith to sign up if it's your first time. The meeting is open to CG members only.
The meeting will be on a zoom.us video conference. Installation is required, see the calendar invite.
- Opening, welcome and roll call
- Opening of the meeting
- Introduction of attendees
- Find volunteers for note taking (acting chair to volunteer)
- Adoption of the agenda
- Proposals and discussions
- Review of action items from prior meeting.
- POLL: WASI subgroup chair
- POLL: WASI subgroup charter
- proposal here derived from the Debugging Subgroup's charter
- [WASI] Can we land WASI libc in WebAssembly/reference-sysroot?
- Presentation: K language and wasm
- Discuss Community Group chat and increasing inclusiveness at the community group meetings.
- Closure
None
None
- Adam Klein
- Alex Crichton
- Alon Zakai
- Andreas Rossberg
- Arun Purushan
- Ben Smith
- Ben Titzer
- Conrad Watt
- Dan Gohman
- Daniel Ehrenberg
- Derek Schuff
- Everett Hildenbrandt
- Flaki
- Francis McCabe
- Jay Phelps
- Luke Imhoff
- Luke Wagner
- Maher Jendoubi
- Mark Miller
- Pat Hickey
- Paul Dworzanksi
- Peter Jensen
- Richard Winterton
- Sam Clegg
- Sergey Rubanov
- Sven Sauleau
- TatWai Chong
- Thomas Lively
- Till Schneidereit
- Ulrik Sorber
- Venkat
Jay seconds
BS: So let’s start off with the WASI subgroup chair. I’ll take about this briefly. So when we did the subgroup in the past we just sort of nominated a chair -- not really, but I mean, people who proposed the subgroup became the chairs. I think that’s reasonable to do here, too. But I did want to bring it in front of the community group to have it official and down in writing. Obviously Dan Gohman has been spending pretty much all the time working on this. So I think it’s reasonable for him to be the subgroup chair of the WASI subgroup. But I’d like to put that to a poll in the group. Is everyone OK with that? Any questions about it?
BS: OK, let’s go to the poll.
Dan Gohman as WASI subgroup chair?
| SF | F | N | A | SA |
|---|---|---|---|---|
| 21 | 2 | 0 | 0 | 0 |
DG: How about a chair as a backup, is that worth doing now?
BS: If we want to have an additional chair, we can do that now. But we can also do it later. Does anyone want to be co-chair?
SBC: I’m happy to step up to co-chair if we think that’s necessary.
Sam Clegg as subgroup co-chair?
Flaki: Should we reach out to group about this?
BS: People on this group will probably be the ones who’d be interested in doing this.
TS: I don’t think waiting two weeks here would make a difference, we could just go ahead.
Flaki: no objections
BS: Any concerns over the subgroup charter?
derived from the Debugging Subgroup's charter
TS: There’s nothing controversial in it, it’s the same boilerplate that we used for previous subgroups.
BS: Unanimous consent
BS: There’s a PR that’s in the reference sysroot that Dan has been keeping up to date with the WASI original source that was in CraneStation and we wanted to make sure that we could land this, but we wanted to bring it to the CG first.
DG: It’s a libc implementation, based on code from cloudlibc, libpreopen and musl. If there are technical concerns I think we can address those after we land. There’s nothing that’s going to be fixed in stone here. I think the biggest question raised so far is the license. Musl is an MIT license and at the moment there’s no other MIT license code in the webassembly org. Is this OK? I don’t know why it wouldn’t be, but I’m interested if anyone has ideas why it would.
BS: Yeah, curious if anyone knows more about the specifics of how we were doing licensing in the past, I wasn’t really involved in those conversations. Our current license is Apache 2.
JP: There were discussions about Apache vs MIT before in the past. The difference being the explicit patent grant versus the ambiguous… MIT doesn’t explicitly call it out. This came up with Binaryen.
BS: Yes, I remember that too. I’m not sure how that works with changes going forward. The code we copied would be MIT, but how would new could work?
JP: Could we get legal guidance from W3C?
BS: I Could talk to Eric about this. I don’t want to hold up the PR though.
DS: One other issue could be the Patent Grant that need to be signed. If we say “no contributions until you are in the CG”, and that should have us covered.
TS: Another question is whether all of musl should be considered part of our implementation, we might want to ask our lawyer/W3C.
BS: I can follow up with Eric, although I would prefer not to stall this further. I think DS’s suggestion is a reasonable/good faith one.
JP: As a counterpoint, just contributing does not mean one is allowed to grant a patent. That said this may not be an issue here.
BS: ..
SBC: This could become a natural artifact of the spec.
DG: This is more a layer on top of the specification, maintained by the CG.
BS: In a way it could end up being similar to the tools that we already provide -- not part of the specification, but a convenience for working with the spec product. Sounds like we have enough concerns that we should seek guidance from lawyers first, instead of just landing.
SBC: We already have other licenses in the repo, so it wouldn’t hurt to get legal guidance overall.
AI[BS]: talk to eric about licenses
JP: Could we still vote, pending no concerns are raised by legal?
BS: Sure
SBC: I would have some small concerns, but nothing major, I could just comment on the PR.
BS: More looking for general problems, overall direction of the PR.
SBC: Should we find an alternative for musl, since it’s so linux-specific?
DG: In this case we should just discuss offline
SBC: I’m happy to see this land, actually, if legal is fine.
BS: We could just come back in two weeks, and see if any concerns emerge.
BS: [technical issues on the connection side]
SR: I have found that our IRC channels are not very popular due to barriers of entry in accessing them. As far as I know Spectrum.chat (owned by GitHub) and also Gitter meet these requirements, and Discord (used by many communities including React, Rust/rustwasm) might be a popular choice.
SR: I helped with run Russian-speaking web assembly community group chat and it’s on telegram. It’s the most popular in Russia, not in the world, so maybe not a good choice. It’s the biggest chat I found, 300 people. We even have english speaking people there. And some core contributors from AssemblyScript, with experience in emscripten and rust. Building a community and helping each other, and were starting a meetup soon in Moscow. I think it would be great to have an official chat, and maybe even a repository or website where people can share links to local meetups. AFAIK there are a number of meetups already, SF, London, Munich, Moscow. Maybe we should have another place where people can find this.
SR: I also found this link on a website, which is kind of outdated, maybe we should also do something with this. I think that web chat can help us to realize what our next steps should be to increase inclusiveness. In our Russian-speaking chat, we collected FAQs, and made a list of links explaining how wasm works. What do people think about this? I think the hardest question is what to use here -- I think slack is not great because it doesn’t have history or logs as far as I know. It’s also hard to sign up. Maybe something people have good experience with Discord or Gitter.
TS: We might want to consider Discord. It has a pretty large community behind it, it is possible to have stable invite links to channels). I could prepare a bit more information on this if people would be interested (by talking to some Rust people) for next time.
SR: Reached out to Ashley Williams, but haven’t received a response yet.
BS: Perhaps we should find a champion for this (maybe SR or TS?). We should also figure out what to do with webassembly.org. Does that sound good to everyone?
JP: [Requested that official CG discussions and community support be clearly separated by channels], I’ve had issues with noise in the past -- too much confusion about implementing and using wasm.
JP: I used gitter before with OSS projects, but exposure to search engines is not great. It does have an archive, but if people are searching for things it is hard to find them. Not sure if others have better experience.
Flaki: We have been experimenting with Spectrum, it has a nice properties, doesn’t replace an actual chat client. Has some problems, not the most stable but is promising.
TS: Happy to make a case for Discord for next meeting -- the rust community has had good experience with this, multiple channels, logs, the features we need. I don’t think we should make a choice right now.
BS: Makes sense. We can put this conversation on hold until next time, and have the conversation after the presentation.
BS: You’re on the call now?
EH: Yes, finally was able to join. Also Dwight (?) another engineer at runtime verification, Rikard (?) university of Chalmers.
EH: Would like to give a tour through the KWasm semantics. Does that sound good?
EH: First I’ll start with this presentation I gave at Edcon.
EH: Rikard has been helping me a lot with KWasm, he can chime in on technical details. We’ll go through this quickly.
EH: Idea with K is to write down your formal semantics once, and syntax and semantics and all tools derive from single golden truth.
MM: [issues w/ screen sharing]
EH: We have the semantics of several large languages, JavaScript, Python, EVM LLVM. C++ is WIP, Solidity is WIP. All these tools except test case generation and compiler is derived from the semantics. Compiler is in the prototyping phase, test case generation -- we have a road map for it, general plan for it but we haven’t implemented yet. Focus of this talk was the deductive program verifier, because that’s what people were interested in, so that’s highlighted here.
EH: To specify program in K, you have to give syntax of language, and configuration (which is like state monad), and rules which describe small-step operational semantics of language.
EH: People are mostly interested in the Wasm semantics probably. The way the semantics are broken down there are two files -- operational semantics, we assume validation has already happened. If that hasn’t happened, then the semantics will get stuck. Two files data.md/wasm.md are the two files interesting. Data defines algebraic data structures, used in wasm.md to define the semantics.
EH: data.md define our basic types, i32 and i64. This in quotes means that this token literal is an inhabitant of this sort ival type, and that generates a parser for us. Here we can subsort all the ival types and fval types into a sortval type.
EH: Here’s some examples of declaring type constructors. List of valtype is valtypes, and the list is separated with empty syntax. Valtypes with square braces around it is a vec type. A vectype with arrow between it is a func type.
EH: Here’s an example of a recursively defined function. It uses a function annotation, says we can take two valtypes and append them to make a new valtype. It will look a lot like a conslist append operator in a function programming language.
EH: More helpers functions. Now we get to values, number is an int or float. Semantics we do dynamic typing, we store the width with each number. This is a data constructor, so if we have left angle bracket, ival type, and right angle bracket and int that makes an ival. That will be used in semantics later. Then we subsort everything into a supersort val to complete our subsort hierarchy. We add a special value called undefined.
EH: The chop function is our workhorse, it makes sure things are within their correct range. If we chop a typed value N, and it’s in this itype here, we take the mod of the pow of the valtype here, so we get 232 for i32, and 264 for i64.
EH: Here we tell it, don’t simplify this chop function if any of its arguments are symbolic, so this is useful if we want to axiomize chop instead of simplifying it. More helpers for signed/unsigned numbers. Some things that lift the kbool sort into integers, for storing on the stack. Some stack operations, we define stack as a conslist of stack items, and stack items are values. Some other stack operations. Local memory is a map, we can do bulk updates of the map. We have to split the integer your storing into a set of bytes.
EH: This was just to warm up with K a bit, most of this data semantics are pretty similar to Wasm. Moving on to K’s WebAssembly semantics, here we have been trying to get the records from the Wasm spec and just translate them into K. Some cases we had to deviate a little bit.
EH: K cell -- that is a syntax declaration. This is our instruction stack on the K cell, we have a separate stack for values. We deviate from wasm spec here. He have the current frame, we have a bunch of addresses, as well as local variables, and portion of module instance we support (globals, mem addresses). Basically, you have to say the function definition has a function name, a chunk of code (by default empty list), some type (domain and range, so this is a functype), some locals (vectype), and addresses that that function can see in scope. We try to do it literately, so the code you’re seeing here in markdown is the source code.
EH: When we get a list of instructions, we have to sequence it out with followed-by operator. This lets us pattern match directly on i in later rules, and omit everything else with the …. Let’s look at an actual opcode. We declare the syntax of folded and unfolded form, of the opcodes. Here is the unfolded form… if you have that form on the front of the kcell, then we sequence it out, evaluate first, then evaluate second and deal with unfolded form. For unfolded form, we check first if the itype is the same as the first two, if it is then we apply the itype binop to the two integer arguments. Almost like refolding it back up. That let’s us define the semantics of each opcode separately. Similar to the spec, we have binary arithmetic operators. We use the chop function to make sure values stay within bounds. Most of the opcodes are straightforward. Let’s try to get to something more interesting. Stack manipulation operators -- like select, has folded and unfolded form. Checks for i32, then numbers (which are vals), checks to see if they have the same type.
EH: Going to scroll more quickly through, to show you what we’ve implemented. Labels, blocks, breaks, conditional breaks, if-then-else, loops, Rikard recently implemented memory. We have function declarations as well.
EH: Normally in wasm you have to declare an entire wasm module, but we are more lenient. We don’t require there to be a module in scope. For modules, we take a list of instructions and execute them. Later when we finish module semantics, we close the module which loads the current state of the VM, which moves it into a module that you have to point to.
EH: We don’t currently have any floating point, since our target is K eWASM, for eWASM happening with ethereum, still need module semantics and table semantics. I can take some questions now, or show a proof.
CW: The K framework allows you to generate verification tools from a semantic definition. Do you have any ability to verify language level properties of the specification itself. How does this relate to existing mechanisation.
EH: There are some tools that let you do that, but won’t compare to what you can do in isabel. The reachability logic prover for instance, the strength is that it is fast, you don’t have to manually specify how to find the proof. We’re only working in reachability logic, we can model check to find proofs that some reachability property holds. It’s been adequate for us for functional correctness verification. We’re able to scale up to large programs using our evm semantics.
??: Because we can use generate an interpreter from the semantics, we use the tests associated with the semantics to at least test that they behave correctly when executed on various concrete inputs. This is one way we guarantee we have correct semantics, it’s not a formal reasoning about the properties.
CW: Thanks, that’s helpful.
AR: Can you share how you model branches? It recall it was difficult for isabel [CW: main difficulty was for the type soundness proof, which is not expressible in this mechanization]. I would be curious to see how this turns out in K.
EH: In the K specification I think it turns out quite nice.
[some technical issues]
EH: This is the meat of how this context operator is implemented. What makes it nice, is that we separate out the instruction stack from the value stack. First we have labels, in the wasm spec the labels are annotated with how many values -- the return amount. The list of instructions, we also store the current stack at the time the label is created. Instead of the number, we store the vector of types. It probably isn’t necessary if we run it through the validator.
EH: If we hit a label, we replace the current stack with the stack that the label is storing, but we take the types off the top of the current stack. This take operation is like the take operation in haskell, but this takes the first types that match from the stack.
AR: This is when you exit the label?
EH: Yeah, when a label comes to the front of the kcell, then we are exiting into the continuation. A block of some type, we will end up executing the block, but then create a label with the empty continuation, but the current stack is stored off in that label, then the stack is zeroed out for the execution of the block. This is the block balancing stuff.
AR: Why did you have to do the take there? Validation ensures that you need to take the entire stack.
EH: True, I wanted to typecheck as much as possible. This is an inefficiency. This is a take that typechecks as it goes.
BS: [break to mention that we are at time]
[presentation continues]