4 ms·

Re-fixing Servo's event-loop

117 points by Ygg2 2y ago

baq 2y ago
Didn't expect to find a TLA spec here! Criminally underused tool in our industry.
- nextaccountic 2y ago
  There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case? Or maybe https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom
- JasonSage 2y ago
  I also didn't expect to find it, partially because I've had basically no exposure to it... I've heard about these formal verification tools but I never really grasped them or felt like they applied to any of the problem domains I work in. But WOW did the example here really drove home how it could be a very useful tool for me. I can think of a few projects I've worked on or reviewed in the last year where I'd have considered using this, and still am.
- pjmlp 2y ago
  The problem with most of these tools is the same as when we got the UML driven development craziness, most of them don't map to the actuall source code being written, and most often than not, mistakes get introduced as the actual implementation doesn't match the model. What the industry is missing is more adoption of Design by Contract, formal verification clauses (SPARK and Frama-C style), Type Driven Development, across mainstream languages, alongside more love for stuff like Dafny, F* and such.
- romac 2y ago
  If you haven't seen those already, you might also want to check out: - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org) - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)
  - baq 2y ago
    Quint looks great, thanks for the link!
bsaul 2y ago
I'm so glad the industry starts adopting formal proofs more and more... After 20 years in the industry i still feel like a caveman, coding as best as i can, hoping nothing bad will happen (and then sighing at the sight of the 100ks line counts of my project). Maybe having more powerful code generators like LLMs will shift us toward spending more time on specification and modelling ? Let's hope so.
- canadianfella 2y ago
  [dead]
- diggan 2y ago
  Some (balanced) automated testing gets you away from "hoping nothing bad will happen" while not having to spend a year coming up with a formal proof for your program. Worth testing if you haven't ;)
  - bsaul 2y ago
    of course, i do test. But let's be honest, if the person writing the tests is the same as the one writing the code, chances are the tests won't discover flaws in the model of the original design.
    - sanxiyn 2y ago
      Try property testing. Property tests written by myself routinely discover bugs in my codes.
    - dllthomas 2y ago
      I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove. Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
  - 2y ago
aumerle 2y ago
The end of the article says the bug isn't fixed, so presumably, the root cause identification was wrong?
proneb1rd 2y ago
This is how medium blogs look like. I can’t believe people still post there https://imgur.com/a/2PpS14h https://imgur.com/a/2PpS14h
- deleted 2y ago
  [deleted]
- touwer 2y ago
  Imgur is not much better ;)
  - pests 2y ago
    It's so bad it's funny https://imgur.com/a/aBfSkEV https://imgur.com/a/aBfSkEV
- wodenokoto 2y ago
  I think medium still does a lot of really good SEO for free. My last company moved from self-hosting to medium because the same content on medium drove more views and generated more leads. But this was a few years ago, so maybe this effect has since collapsed on itself.

117 points by Ygg2 2y ago

baq 2y ago

Didn't expect to find a TLA spec here! Criminally underused tool in our industry.

nextaccountic 2y ago
There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case? Or maybe https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom
JasonSage 2y ago
I also didn't expect to find it, partially because I've had basically no exposure to it... I've heard about these formal verification tools but I never really grasped them or felt like they applied to any of the problem domains I work in. But WOW did the example here really drove home how it could be a very useful tool for me. I can think of a few projects I've worked on or reviewed in the last year where I'd have considered using this, and still am.
pjmlp 2y ago
The problem with most of these tools is the same as when we got the UML driven development craziness, most of them don't map to the actuall source code being written, and most often than not, mistakes get introduced as the actual implementation doesn't match the model. What the industry is missing is more adoption of Design by Contract, formal verification clauses (SPARK and Frama-C style), Type Driven Development, across mainstream languages, alongside more love for stuff like Dafny, F* and such.
romac 2y ago
If you haven't seen those already, you might also want to check out: - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org) - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)
- baq 2y ago
  Quint looks great, thanks for the link!

bsaul 2y ago

I'm so glad the industry starts adopting formal proofs more and more... After 20 years in the industry i still feel like a caveman, coding as best as i can, hoping nothing bad will happen (and then sighing at the sight of the 100ks line counts of my project). Maybe having more powerful code generators like LLMs will shift us toward spending more time on specification and modelling ? Let's hope so.

canadianfella 2y ago
[dead]
diggan 2y ago
Some (balanced) automated testing gets you away from "hoping nothing bad will happen" while not having to spend a year coming up with a formal proof for your program. Worth testing if you haven't ;)
- bsaul 2y ago
  of course, i do test. But let's be honest, if the person writing the tests is the same as the one writing the code, chances are the tests won't discover flaws in the model of the original design.
  - sanxiyn 2y ago
    Try property testing. Property tests written by myself routinely discover bugs in my codes.
  - dllthomas 2y ago
    I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove. Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
- 2y ago

aumerle 2y ago

The end of the article says the bug isn't fixed, so presumably, the root cause identification was wrong?

proneb1rd 2y ago

This is how medium blogs look like. I can’t believe people still post there https://imgur.com/a/2PpS14h https://imgur.com/a/2PpS14h

deleted 2y ago
[deleted]
touwer 2y ago
Imgur is not much better ;)
- pests 2y ago
  It's so bad it's funny https://imgur.com/a/aBfSkEV https://imgur.com/a/aBfSkEV
wodenokoto 2y ago
I think medium still does a lot of really good SEO for free. My last company moved from self-hosting to medium because the same content on medium drove more views and generated more leads. But this was a few years ago, so maybe this effect has since collapsed on itself.