switch to producing a checker in C
This might seem like a bit of an odd direction to go in. However, I've realised the advantages we get from C++ in the checker are actually not especially significant. The main strengths in code like this are being able to write static code ahead of time using templates and then instantiate it during generation. However, we need to emit custom classes for almost everything non-trivial (e.g. records). None of the data structures we need are especially complex, except the state set and queue which I think we're best outsourcing. My hypothesis is that this combination (C source + GLib) can beat a C++ solution, in terms of runtime and memory usage. I don't know whether this will pan out, but interesting to try. One notable thing we lost in this change was exception support. Exceptions were shaping up to be quite an elegant mechanism for reporting a checker failure. However, my long term plan was always to remove them (or at least make them optional) to allow better interoperability with other languages. I think we should probably still be able to come up with a performance, thread-safe solution.
parent
771fa4c0
Please register or sign in to comment