Can we create deadlock free computation in the type system?

76 points gigapiksel

A little while ago I pondered whether we can use the type system to guarantee deadlock-free computation, in a directed acyclic computational graph. I had a bit of a deeper think today, realising that at least for the case of a single lock, we can just ensure that any computational steps don't contain shared mutexes. This could be done with an auto trait and a negative trait implementation for Mutex<T>. I've done that here with a trait MutexFree. For now I only created a struct for repeated operation on state, and a method for running operations in parallel, but it would be pretty straightforward to introduce channels as a method of composing operations. Does anyone know if something like this is already being done?

I think an interesting next step would be figuring out how to handle multiple distinct mutexes, also using something like a directed acyclic graph to prevent one thread locking the first mutex and waiting for a lock on the second, while the second thread locks the second mutex then tries to lock the first one. I think something like this could be encapsulated in the traits, so that a trait implementation local Lockable type takes ownership of both mutexes after which a computation will have access to both, but must always lock both in order.