Message-ID: <725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com>
Date: Thu, 13 Oct 2022 08:42:22 -0700
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.2.1
Content-Language: en-US
To: ~skeeto/public-inbox@lists.sr.ht
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Subject: relationship to model checking
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit

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