Message-ID: <c7d4ec1f-3f3d-c579-1955-eb0cce99883b@gmail.com>
Date: Sun, 16 Oct 2022 11:30:24 -0700
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.3.1
Subject: Re: relationship to model checking
To: Christopher Wellons <wellons@nullprogram.com>
Cc: ~skeeto/public-inbox@lists.sr.ht
References: <725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com>
 <20221016153801.fieqzt3ianrujnxd@nullprogram.com>
Content-Language: en-US
From: Matthew Fernandez <matthew.fernandez@gmail.com>
In-Reply-To: <20221016153801.fieqzt3ianrujnxd@nullprogram.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit



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 :)