One the things mentioned in class was that lock-free programming is often error-prone because it's difficult to think through all the possible cases, especially when memory allocation/deallocation is involved. Here is an interesting paper on creating models for formally verifying the correctness of lock-free programs Link.
One the things mentioned in class was that lock-free programming is often error-prone because it's difficult to think through all the possible cases, especially when memory allocation/deallocation is involved. Here is an interesting paper on creating models for formally verifying the correctness of lock-free programs Link.