It seems like implementing even the simplest data structures like linked lists correctly requires a PhD thesis with several revisions. Is there actual correct code that use fine grained locks or a lock-free design? What methods do people use to debug or prove code?
kayvonf
Absolutely. It's not easy, but lock-free data structures are in common use. For example, Java's concurrent HashMap is a lock-free implementation.
apoms
To restate what Kavyon said in point one...
The move to finer grained locks is motivated by a desired to increase potential parallelism. Yet as we increase the number of locks we generally incur the need to touch multiple locks in the course of a single operation. Each additional lock adds a fixed amount of overhead to the operation. So as we make our locking granularity finer, and thus the ability for smaller units of work to happen simultaneously, we inherently increase the fixed cost of those smaller units of work until the overhead becomes a dominating factor.
Perhaps this suggests a hybrid strategy where we have both fine granularity locks and a larger coarse lock. When we know we are going to perform an operation that operates across the entire data structure, for example a rehash on a hash table, we can acquire the global lock and perform our actions on the data structure without having to incur the overhead of acquiring every fine grained lock.
It seems like implementing even the simplest data structures like linked lists correctly requires a PhD thesis with several revisions. Is there actual correct code that use fine grained locks or a lock-free design? What methods do people use to debug or prove code?
Absolutely. It's not easy, but lock-free data structures are in common use. For example, Java's concurrent HashMap is a lock-free implementation.
To restate what Kavyon said in point one...
The move to finer grained locks is motivated by a desired to increase potential parallelism. Yet as we increase the number of locks we generally incur the need to touch multiple locks in the course of a single operation. Each additional lock adds a fixed amount of overhead to the operation. So as we make our locking granularity finer, and thus the ability for smaller units of work to happen simultaneously, we inherently increase the fixed cost of those smaller units of work until the overhead becomes a dominating factor.
Perhaps this suggests a hybrid strategy where we have both fine granularity locks and a larger coarse lock. When we know we are going to perform an operation that operates across the entire data structure, for example a rehash on a hash table, we can acquire the global lock and perform our actions on the data structure without having to incur the overhead of acquiring every fine grained lock.