‹ BackHN Continuity

Thread

Book review: Is parallel programming hard, and, if so, what can you do about it?

149 points · 66 comments · ahelwer

  1. thomasahle · · focus · HN ↗
    Parallel programming is a great application for LLM correctness proofs in Lean.

    You can't unit test your way out, but if you care about the code's correctness, today there's a way.

    1. tintor · · focus · HN ↗
      Mix of different types of tests helps.

      Best examples are SQLite and Jepsen test suites for dbms engines.

      <a href="https:&#x2F;&#x2F;jepsen.io&#x2F;" rel="nofollow">https:&#x2F;&#x2F;jepsen.io&#x2F;

    2. 6gvONxR4sf7o · · focus · HN ↗
      My experience has been the opposite. If lean had linear types (or separation types), it would be, but as it is, Lean&#x27;s just a little bit too focused on talking about results to tidily talk about how those results are computed.
      1. winwang · · focus · HN ↗
        I don&#x27;t know. For many operations, you can encode &quot;how&quot; by saying &quot;under any permutation of this sequence of applications&quot;. At least, for EREW machines.
    3. vitalnodo · · focus · HN ↗
      As I found out recently, there&#x27;s a lighter option: model checkers like Spin. You describe your synchronization logic in a small modeling language (Promela), and Spin tries every possible interleaving of that model.
Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.