1. Jun 01, 2018
  2. May 31, 2018
  3. May 24, 2018
    • Matthew Fernandez's avatar
      d5ad3531
    • Matthew Fernandez's avatar
      switch to a higher performance set implementation · 5637524b
      Matthew Fernandez authored
      Taking a leaf out of some academic literature, this commit implements a simpler
      but more high performance state set implementation. It's essentially an open
      addressed hash table with linear probing, but with the ability to expand the
      capacity as it fills up. It's not very well documented in the source yet because
      it's only half finished. We also need to parallelise the expansion and make it
      thread-safe, but I think this is best postponed until we regain multithreaded
      checking.
      
      This also modifies a command-line flag and introduces a new one:
      
        * --set-capacity: This now specifies the initial size of the set that is
          allocated. That is, if you pass 'x', a set size will be allocated such that
          when full it will occupy 'x' bytes. This is perhaps counterintuitive and
          maybe we should consider renaming this flag.
        * --set-expand-threshold: The percentage occupancy at which we consider set
          insertion inefficient and choose to expand the set.
      
      TODO:
      
        * Option to set "never" for --set-expand-threshold. This would just terminate
          when we fill the set.
        * More precise initial capacity calculation. See the FIXME around this.
        * Parallelisation of the expansion logic.
      
      With these changes long-running2 is checkable using --set-capacity 8589934592
      --set-expand-threshold 100 in 79 seconds on a single core. It is actually slowed
      by hitting swap on the machine I'm on (synecdoche). It looks like we could do it
      closer to 45-50 seconds without touching swap.
      5637524b
  4. May 14, 2018
    • Matthew Fernandez's avatar
      switch to using xxHash for hashing states · f67cf8c8
      Matthew Fernandez authored
      By using a proper hashing function we get a fairly dramatic speed up. This now
      makes checking long-running2 practical. We get 453 seconds on our current
      representative platform. Note, this is still single-threaded.
      
      This commit contains sources from xxHash v0.6.5. xxhash.c from that release has
      been pasted into xxhash.h so that we can emit the checker as a single source
      file.
      f67cf8c8
    • Matthew Fernandez's avatar
      expand hash buckets to 8MB · 7f193777
      Matthew Fernandez authored
      This -- combined with an upcoming change to a more practical hash function --
      results in fewer hash collisions and thus vastly improved performance of
      set_insert.
      7f193777
  5. May 13, 2018
    • Matthew Fernandez's avatar
      include linked-list pointer in the state data structure · 160ace98
      Matthew Fernandez authored
      This saves us having to do an extra allocation during insertion into the state
      set, speeding up checking by ~20%. Checking is still extremely slow, but this is
      just an obvious piece of low hanging optimisation fruit.
      160ace98
    • Matthew Fernandez's avatar
      103b7379
    • Matthew Fernandez's avatar
      3532e97f
    • Matthew Fernandez's avatar
      rewrite checker in C · 06053b03
      Matthew Fernandez authored
      We now generate the checker itself as C, rather than C++. My current intuition
      is that we can beat the speed of the C++ checker by moving to C. By making our
      operations more transparent to the compiler we should be able to (a) move type
      checking to Rumur and avoid some coercion hell in the checker as well as (b)
      essentially force devirtualising all function calls.
      
      Note that this commit drops a significant amount of functionality:
      
        * TBB support
        * Useful state hash (to be reintroduced later)
        * Multithreaded support (to be reintroduced later)
        * Support for a fixed-size seen set
        * Support for a fixed-size queue
      06053b03
  6. Mar 26, 2018
  7. Mar 20, 2018
  8. Mar 13, 2018
  9. Mar 07, 2018
    • Matthew Fernandez's avatar
      write some more effusive --help text · 0bbe7c7d
      Matthew Fernandez authored
      We should really convert this to a manpage instead.
      0bbe7c7d
    • Matthew Fernandez's avatar
      introduce an option to use Intel Thread Building Blocks · 38cc3ee9
      Matthew Fernandez authored
      This commit introduces a new command line option, --tbb, that enables the use of
      Intel Thread Building Blocks' tbb::concurrent_unordered_set for the
      multithreaded checker. For our current work horse, long-running2, this appears
      to make no discernible difference in its runtime characteristics. However, I've
      still committed this because it's relatively low overhead and I wonder if it may
      prove useful on future models.
      38cc3ee9
  10. Mar 04, 2018