Proving soundness

[sagudev]

So I was thinking how can we prove that what we do is actually correct (mainly we are interested in correctness of high-level wrappers so mozjs).

Ideally we would just run MIRI but AFAIK we cannot (yet: rust-lang/miri#11) because FFI and other syscalls. So my idea is to write dummy mozjs-sys that can be used in place of real mozjs, that would emulate context/rooting/tracing/handles and GC (we do not need to do actual js execution). This way I think it's feasible to run MIRI on subset of mozjs (and it's test/examples).

Side-quest: How hard would it be to use pure rust JS engine for this (boa)? Probably not much and we could cover more, but SM works in a uniqe way.

[jschwe]

Side-quest: How hard would it be to use pure rust JS engine for this (boa)?

dummy mozjs-sys that can be used in place of real mozjs, that would emulate context/rooting/tracing/handles and GC

How would you combine those two things (existing rust JS engine + emulate SM GC related behavior)?

[sagudev]

Side-quest: How hard would it be to use pure rust JS engine for this (boa)?

dummy mozjs-sys that can be used in place of real mozjs, that would emulate context/rooting/tracing/handles and GC

How would you combine those two things (existing rust JS engine + emulate SM GC related behavior)?

I would use cargo's patch to override mozjs-sys, then use feature gating in mozjs so we would only need to implement subset of mozjs-sys. But that would only be used for testing.

[jschwe]

For miri to report issues, wouldn't the mock need to GC in the same way (or more often) than SM? I'm not very familiar with SM, but it sounds like a hard task to get right to me.

[sagudev]

For miri to report issues, wouldn't the mock need to GC in the same way (or more often) than SM? I'm not very familiar with SM, but it sounds like a hard task to get right to me.

For GC we would only do trace part (this should tell us if something is wrong with aliasing). Each SM function (that can GC) would trigger tracing, but otherwise most of them would be nop. I we start small (cx, rooting, primitive tracer) I think we could quickly get the prototype, that works on small tests.

With that being said, I do not plan to work on it this year, but hopefully I will be to do quick prototype in the summer and if it works well I think I can take on this in the fall and write some more docs on GC/SM/Servo.

[gmorenz]

I love the idea. I think it might be pretty hard (though not impossible). I'm particularly eyeing soundness claims I remember making when analyzing the code like this one that all but relies on the ffi hiding what is actually happening from rustc.

I read this as &Heap<T> -> *mut T (which would be the forbidden pattern), but it's actually &Heap<T> -> *mut Heap<T>, and while you're not allowed to write through that pointer, you are allowed to read through it, to call .get() on the UnsafeCell, and write through the returned *mut T. The *mut Heap<T> is immediately passed off to C and the rust compiler can't "prove" that the foreign C code is writing directly to it without calling .get on an UnsafeCell to get a valid pointer first. So this shouldn't be able to result in undefined behavior.

Of course if the rust replacement does what the C++ side "should" (according to rustc) be doing then it wouldn't be an issue.

The "side-quest" of making at least the core of mozjs able to work on top of boa (or nova/brimstone to list other rust js engines) might involve cleaning up these APIs enough that there aren't tortured justifications like this.

[sagudev]

I just thought about this yesterday and running miri only on mozjs might not be as useful as I initially though as we have not have enough tests and servo uses many other stuff (there is practically no tracing tests here). Anyway this issue is mainly about throwing ideas around.