[HN Gopher] GenMC: Model checking for concurrent C programs
       ___________________________________________________________________
        
       GenMC: Model checking for concurrent C programs
        
       Author : todsacerdoti
       Score  : 51 points
       Date   : 2024-11-10 03:45 UTC (19 hours ago)
        
 (HTM) web link (plv.mpi-sws.org)
 (TXT) w3m dump (plv.mpi-sws.org)
        
       | djoldman wrote:
       | From: https://github.com/MPI-SWS/genmc/blob/master/doc/manual.md
       | 
       | Basic Usage
       | 
       | A generic invocation of GenMC resembles the following:
       | 
       | genmc [OPTIONS] -- [CFLAGS] <file>
       | 
       | ...
       | 
       | Note that, in order for GenMC to be able to verify it, file needs
       | to meet two requirements: finiteness and data-determinism.
       | Finiteness means that all tests need to have finite traces, i.e.,
       | no infinite loops (these need to be bounded; see Section 2.3).
       | Data-determinism means that the code under test should be data-
       | deterministic, i.e., not perform actions like calling rand(),
       | performing actions based on user input or the clock, etc. In
       | other words, all non-determinism should originate either from the
       | scheduler or the underlying (weak) memory model.
       | 
       | As long as these requirements as satisfied, GenMC will detect
       | safety errors, races on non-atomic variables, as well as some
       | memory errors (e.g., double-free error). Users can provide safety
       | specifications for their programs by using assert() statements.
       | 
       | **
       | 
       | I wonder how much this affects usefulness. How often is this the
       | case?
        
         | ronsor wrote:
         | In a proper testing environment, you should be using a
         | deterministic seeded PRNG, simulated user input, and a
         | simulated/fake clock.
        
         | 95014_refugee wrote:
         | It's always a compromise.
         | 
         | Part of the exercise, whether it be making an existing codebase
         | amenable to verification, or standing up a new one designed for
         | it from scratch, is to identify, contain, and comprehend
         | sources of entropy within the system.
         | 
         | At test time, you explore (as much as possible) the state space
         | by replacing these components with data-deterministic mocks. On
         | a run-to-run basis you can then vary the characteristics of the
         | data they return; either with a set of derived known-edgy
         | values, or by fuzzing, or a variety of the two.
         | 
         | This sounds daunting, and for a pre-existing codebase it can be
         | a lot of work, but the upside is very often a substantial
         | improvement in the robustness of and achievable confidence in
         | the implementation.
        
       ___________________________________________________________________
       (page generated 2024-11-10 23:01 UTC)