pypy/pypy.org

Fixing a Bug in PyPy's Incremental GC | PyPy

Closed this issue · 4 comments

rejones commented

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

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

rejones commented

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

This has broadened my understanding of PYPY's GC.