search

pypy / pypy.org

Sources for website at https://www.pypy.org
33 stars 11 forks source link

Fixing a Bug in PyPy's Incremental GC | PyPy #113

Open utterances-bot opened 3 months ago

utterances-bot commented 3 months ago

Fixing a Bug in PyPy's Incremental GC | PyPy

https://www.pypy.org/posts/2024/03/fixing-bug-incremental-gc.html

rejones commented 3 months ago

Interesting account of GC bug hunting. Thanks for sharing.

One question you raised was the use of formal approaches to checking the correctness of GC code. When we built the Transactional Sapphire GC (https://doi.org/10.1145/3226225), we found model checking with SPIN to be very helpful. TS is a fully concurrent GC (no pauses) so has lots of opportunities for getting things wrong.

We found model checking with SPIN to be fairly straightforward and gave us confidence in our algorithms, and I’ve used it again to check concurrent algorithms. However, there are things to be borne in mind when using it.

  1. You need to write a model for each scenario you want to check. There may be many. But we simply checked those that we had concerns about……

  2. SPIN checks the model (written in Promela), not the actual source code.

cfbolz commented 3 months ago

@rejones thanks a lot for your comment, Richard! The paper looks interesting, thanks for the reference!

rejones commented 3 months ago

There’s also a tech report with more about our SPIN modelling on my GitHub. Can’t remember if we mentioned that in the paper

jws1837 commented 2 months ago

This has broadened my understanding of PYPY's GC.