~skeeto/public-inbox

2 2

relationship to model checking

Matthew Fernandez <matthew.fernandez@gmail.com>
Details
Message ID
<725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com>
DKIM signature
pass
Download raw message
Hi Chris,

I read your recent Dandelions post with fascination as per usual; always 
find your writings interesting and always learn something new!

I was wondering if you ever use tools like model checkers for these 
problems instead of hand-written C? The reason I ask is that I’ve worked 
on several explicit state model checkers in the past and I often 
recognize optimization tricks you employ as patterns I’ve previously 
used in model checkers. For example, many of the bit-packing 
optimizations, canonicalization, some compiler intrinsic tricks, …

The latest model checker I worked on in this style generates a 
multi-threaded C program that uses some lock-free data structures to go 
a bit faster. As someone most comfortable working in C, I often wonder 
whether I myself could hand-write something that outperforms it. That 
is, I’ve tried to encode as much of my knowledge about hand-optimizing C 
as possible into the code generator, but I still have some unanswered 
questions about how close to the limit of my own hand-written C the 
generated code is reaching.

Interested to hear your thoughts on this topic.

Thanks,
Matt
Details
Message ID
<20221016153801.fieqzt3ianrujnxd@nullprogram.com>
In-Reply-To
<725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com> (view parent)
DKIM signature
missing
Download raw message
Thanks for the kind words, Matt! I've dabbled with Prolog, but otherwise 
I've never made use of constraint programming or model checkers. It's 
probably something I should learn, especially if I keep doing this. There 
is a growing number of interesting games from the book (Neutron, Order and 
Chaos, Splatter, Sequencium, Pennywise, Prophecies) that I'd like to 
explore more thoroughly. Do you have recommendations?

While working on Dandelions, I considered a multi-threaded tree search, 
but didn't feel it was worth building the machinery for it, particularly 
because it's ultimately memory constrained. (A branch exploration queue 
with appropriately-sized work chunks, synchronizing memoization, or 
per-thread memoization with even greater memory demands, etc.) Had it been 
pre-built as part of a model checker, I would have used it of course.

> I often wonder whether I myself could hand-write something that 
> outperforms it.

I wouldn't be surprised if a thoughtful, hand-written implementation 
outperforms the generated one, even if you've encoded as much knowledge as 
you can. There's likely still more context to be exploited. On the other 
hand, it sounds like it's already finely-tuned to this narrow problem 
space. Hard to say, especially since I'm not familiar with model checkers.

A couple months ago I showed it's easy to outperform "battle-hardened" 
generic hash tables in compiled languages (C++, Go, etc.) since you 
usually have so much local knowledge to exploit. I've had similar results 
parsing JSON and XML: With a known, fixed schema, a hand-written parser 
can be small and very, very fast vs. a generic parsing library. Here's my 
favorite talk on this subject:

Context is Everything
https://vimeo.com/644068002

Compared to a one-size-fits-all hash table or parser, the gap between 
generated vs. hand-written model checker is probably small. Also, if the 
goal is simply to prove some things about a game, it also probably doesn't 
matter whether you get the answer in 1 minute or 10 minutes. The main 
benefit would be speeding up testing and validation during development, 
after which it matters little. The performance boost could easily cost 
more than what you gain from faster testing (e.g. my decision not to 
bother with multi-threading).
Matthew Fernandez <matthew.fernandez@gmail.com>
Details
Message ID
<c7d4ec1f-3f3d-c579-1955-eb0cce99883b@gmail.com>
In-Reply-To
<20221016153801.fieqzt3ianrujnxd@nullprogram.com> (view parent)
DKIM signature
pass
Download raw message

On 10/16/22 08:38, Christopher Wellons wrote:
> There is a growing number of interesting games from the book (Neutron, 
> Order and Chaos, Splatter, Sequencium, Pennywise, Prophecies) that I'd 
> like to explore more thoroughly. Do you have recommendations?

I assume you mean model checker suggestions, not game suggestions. If I 
can selfishly plug my own tool, https://github.com/smattr/rumur :) It 
doesn’t have great docs on the input language, but you can find copies 
of older Murphi language docs floating around on the internet, e.g. 
https://www.cs.ubc.ca/~ajh/courses/cpsc513/assign-token/User.Manual.

> A couple months ago I showed it's easy to outperform "battle-hardened" 
> generic hash tables in compiled languages (C++, Go, etc.) since you 
> usually have so much local knowledge to exploit. I've had similar 
> results parsing JSON and XML: With a known, fixed schema, a hand-written 
> parser can be small and very, very fast vs. a generic parsing library. 

This matches my own experience too. By essentially dropping some feature 
requirements from a generalized data structure/algorithm, you end up 
easily outperforming the off-the-shelf options.

> Here's my favorite talk on this subject:
> 
> Context is Everything
> https://vimeo.com/644068002

Thanks! I’ll check it out!

> Compared to a one-size-fits-all hash table or parser, the gap between 
> generated vs. hand-written model checker is probably small. Also, if the 
> goal is simply to prove some things about a game, it also probably 
> doesn't matter whether you get the answer in 1 minute or 10 minutes. The 
> main benefit would be speeding up testing and validation during 
> development, after which it matters little. The performance boost could 
> easily cost more than what you gain from faster testing (e.g. my 
> decision not to bother with multi-threading).

This is an interesting perspective. I guess I naïvely assumed runtime 
was a critical factor here because it’s usually been a bottleneck for 
model checking problems for me in the past. I was typically modelling 
some new hardware functionality whose design was being iterated on at 
the same time as we were trying to derive proofs. The runtime for some 
of these models could stretch into days or even weeks. In these cases, 
even complex optimizations that only yielded a <10% speed up were still 
often worth it. Having said that, memory usage was also a constant concern.

Thanks for your reply! Lots of interesting things for me to ponder :)
Reply to thread Export thread (mbox)