1. Jan 20, 2020
  2. Jan 19, 2020
    • Matthew Fernandez's avatar
      juggle SMT test cases to be more effective · 7a33011d
      Matthew Fernandez authored
      Knowing that `|` in Murphi maps to `||` in C, we swap the order of the
      conditionals in the forall test cases to *really* force an undefined read if the
      entire expression is not optimised to `true`.
      7a33011d
    • Matthew Fernandez's avatar
    • Matthew Fernandez's avatar
      enable some now-passing tests · bb1ae8dc
      Matthew Fernandez authored
      bb1ae8dc
    • Matthew Fernandez's avatar
      support for forall in the SMT bridge · 49a0d0df
      Matthew Fernandez authored
      The implementation of this was relatively straightforward, but threw up a last
      minute surprise. Simplification happens first *within* the quantified expression
      with access to the constraints on the quantified variable. So, even without
      explicit support for forall expressions, the following expression:
      
        forall x: 1 .. 2 do x = 1 | x = 2 end
      
      will get simplified to
      
        forall x: 1 .. 2 do true end
      
      We still need explicit forall support to collapse this resulting expression into
      `true` and enable further simplification.
      
      Note that this commit does not yet support custom steps in forall expressions.
      49a0d0df
    • Matthew Fernandez's avatar
      fix: declare a quantifier's decl rather than itself in SMT translation · 2a1b724d
      Matthew Fernandez authored
      This fixes an issue where malformed SMT problems would be produced from
      expressions within quantified sections. The quantified variable would be
      declared using the ID of the quantifier, but then references to it would use the
      ID of the quantifier's contained declaration. As a result, SMT solvers would
      reject the problem for referring to an undeclared variable.
      
      This bug was actually identified while trying to implement forall support in the
      SMT bridge. The upcoming tests for this provoke the bug.
      2a1b724d
    • Matthew Fernandez's avatar
      fix: don't use pointer compression on Linux x32 · 37cfa28a
      Matthew Fernandez authored
      Debian auto builder testing of v2020.01.11-1 exposed that we incorrectly attempt
      pointer compression when using the x32 ABI, under which pointers are 32-bit. We
      now only compress when on Linux x86-64 targeting the standard ABI.
      37cfa28a
    • Matthew Fernandez's avatar
      fix: don't require dword CAS to be inline on ARM · 6d918427
      Matthew Fernandez authored
      While the ARM ISA has support for double-word atomic compare-and-swap,
      apparently compilers do not implement the instructions for this. So in this
      scenario we need to link against libatomic and suppress the lock-free tests from
      the test suite. This was noted during Debian's auto builder testing for
      v2020.01.11-1.
      6d918427
  3. Jan 17, 2020
  4. Jan 12, 2020
  5. Jan 10, 2020
  6. Jan 08, 2020
  7. Jan 07, 2020
  8. Jan 06, 2020
  9. Jan 04, 2020
  10. Jan 03, 2020
    • Matthew Fernandez's avatar
      use a specific value for the tombstone instead of a bit · b517be6b
      Matthew Fernandez authored
      We never actually need to recover the original pointer from a tombstone. We can
      take advantage of this to just use a sentinel value (-1) to represent a
      tombstone. This should speed up any testing against or setting of tombstones,
      but it also removes alignment requirements we have on the state struct.
      b517be6b
  11. Jan 02, 2020