I have finalized the intiial threading model for a program I'm working on, and due to the nature of its enviroment I have to allow deadlocks to occur or loose much of the benift from multithreading. Fortunatly, it also enables easy detection and resolution of deadlocks without rolling anything back; except for one special case though the programmer has to go out of his way to make that one possible and those can still easily be detected though not resolved.

Anyway, I do not think there are any more cases where deadlocking can occur but I'm not 100% certain either. So I'm wondering if there are any good tools or methods for proving that deadlocking is impossible (other than that onbe case I mentioned) in a system of unknown size? The only method I'm aware of is petri nets, though I do not know if that method can be adapted to work with a model of unknown size or not.

I went with this solution as it minimizes locking and ironically, the risk of deadlocks. The source of my issue is that openGL requires every task for a given openGL context to be performed in the same thread, this leads to tasks depending on other tasks for completion. Sometimes these tasks may end up in the same task queue and in the wrong order. The solution I have now simply finds out if a task waits for another in the same queue, and lets the one that is being waited for skip ahead.

Had the requirement to do certain tasks in a given thread not been there, task inter-dependencies would have disappeared and this problem would not be there.

I really wish they would do something about this issue in OGL.

Yeah, this arguably isn't a 'problem' with OpenGL - lots of systems are essentially going to require serialised access to a resource and it's your job to ensure that the series of actions is in the correct order. I would humbly suggest that splitting serialised tasks into multiple queues only to make them block each other based on task ordering is probably the wrong way to go about using task queues.

Had the requirement to do certain tasks in a given thread not been there, task inter-dependencies would have disappeared and this problem would not be there.

That doesn't make sense to me - if the only dependency between tasks is that only one can execute at a time then the ordering issue you mention wouldn't exist. And if there is an ordering issue, then you need to resolve that before attempting to parallelise the tasks because once they're in separate queues, ordering between the queues no longer applies. (Without adding in some sort of global lock which mostly destroys the purpose of having multiple queues.)