3 ms·

Neat! Do you have some pointers to your work? I would be especially interested in example verifications of lock free data structures and in comparing the proof

• pron 11y ago
  > Do you have some pointers to your work? At the moment we're not open-sourcing the spec (I'm an engineer, not an academic) but we might in the future. We've opted not to even try to prove the system's correctness, as that might take decades (it's far more complex than, say, seL4). Instead, we're just formally specifying it, and model-checking it with a finite model. The software in question, however, is itself open-source and is described here: http://blog.paralleluniverse.co/2012/08/20/distributed-b-tree/ http://blog.paralleluniverse.co/2012/08/20/distributed-b-tre... > All the constructions I know use at least second order logic Concurrent algorithms are specified with TLA+ (in the industry, I mean) quite frequently. Also, specifying the memory consistency properties does require second order logic, but as I've shown in another comment, TLA+ handles second-order logic gracefully and in a very straightforward matter (trivially, I would say). You simply write: ∃ ordering ∈ [operations → SequenceOf(Op)] : ConsistencyProperty(ordering[operations])