Lockless algorithms for mere mortals

Posted Aug 1, 2020 17:23 UTC (Sat) by anton (subscriber, #25547)
In reply to: Lockless algorithms for mere mortals by excors
Parent article: Lockless algorithms for mere mortals

Machine-checkability does seem important.

Or one might consider such a requirement (as well as the article) to be an indication that the concepts are too difficult to use. In other cases (e.g., wrt. page colouring), Linus Torvalds has written that he targets hardware that performs well without such complications, and that other hardware deserves what it gets. I think that is a sensible approach for memory ordering as well. Have a model that's easy to understand and performs ok on nice hardware (not sure if nice hardware already exists, but weak consistency certainly does not look nice to me); then hardware designers have an incentive to make their hardware nicer.

It seems to me that all this difficult-to-program memory ordering is there because multi-processors originally come from the supercomputing area, where hardware is still more expensive than software, and hardware designers can get away with making hardware that's hard to program correctly and efficiently.

Lockless algorithms for mere mortals

Posted Aug 3, 2020 10:12 UTC (Mon) by farnz (subscriber, #17727) [Link]

I would say that machine-checkability is necessary but not sufficient. If the rules are so complex to encode that a computer can't verify that you're getting them right, then they are also too complex for a human to get right, too, and they are certainly too complex for a human code reviewer to reliably check.

That said, this is a minimum requirement, as you can have rules that a computer can reliably verify, but that humans get wrong - see DEC Alpha ordering for the classic example.