Srinivas Nayak wrote in comp.programming.threads:
>Please suggest a good book that teaches in great details about the
>theories behind the followings.
>1. shared memory concurrent systems.
>2. message passing concurrent systems.
>3. mutual exclusion.
>5. safety property.
>6. liveness property.
>7. fairness property.
>8. systems with code interleaving (virtual concurrency).
>9. systems with no code interleaving (true concurrency).
>10. atomic operations.
>11. critical sections.
>12. how to code a concurrent system (about programming language
>constructs available for it).
>13. how to mathematically proof the properties.
>14. how to mechanically verify the properties.
>15. blocking synchronization.
>16. non-blocking synchronization.
>Not only the concepts but also that teaches with very simple
>mathematical treatment; axiomatic or linear temporal logic.
>Many of the books I came across are either emphasize one or two topic
>or just provides a conceptual treatment, without mentioning how to
>code a concurrent system, check if it is mathematically or manually
>Please suggest any book or paper where these topics are
>comprehensively covered in great details. Better if all these are
>under a single cover that will be easy to understand under the roof of
>a unifying theory.
>Survey papers of these are also welcome.
For boundedness and deadlocks... - one of
the most important properties .. you can use petri nets
and reason about place invariants equations that you
extract from the resolution of the following equation:
Transpose(vector) * Incidence matrix = 0
and find your vectors...on wich you wil base your reasonning...
you can do the same - place invariants equations... -
and reason about lock and lock-free algorithms...
And you can use also graph reduction techniques...
As an example , suppose that you resolve
your equation Transpose(vector) * Incidence matrix = 0
and find the following equations
P,Q,S,R are all the places in the system...
2 * M(P) M(Q) + M(S) is constant
M(P) + M + M(S) is too equal to a constant
Note also that vector f * M0 (initial marking) = 0
So, it follows - from the equations - that since
M(P) + M + M(S) = C1 , it means that
M(P) <= C1 and M <= C1 and M(S) <= C1
and, from the second invariant equation , we have
that M(Q) <= C2 , this IMPLY that the system is
That's the same thing for deadlocks , you reason
about invariants equations to proove that there is
no deadlock in the system...
Now, if you follow good patterns , that's also good...
And what's a good pattern ?
It's like a THEOREM that we apply in programming...
As an example:
Suppose that or IF - we have two threads that want to aquire
crtitical sections, IF the first thread try to aquire critical section A and
after that critical section B, and the second threads try to
aquire B and A THEN you can have a deadlock in this system.
you see ? it's look like this: IF predicates are meet THEN somethings ...
Now suppose there is many criticals sections... and the first
thread try to aquire A ,B ,C ,D,E,F,G and second thread try to
aquire A,G,C,D,E,F,B that's also a problem ... you can
easily notice it by APPLYING the theorems that we call
You see why good patterns - that looks like theorems -
are also very powerfull ?
That's what we call a good pattern - it's like a theorem ,
and it looks like this: IF predicates are meet THEN somethings ...
There is also good patterns - like theorems - to follow for false
Do you understand why I and others follow also good patterns
- that look like theorems - ?
Think about it...
Amine Moulay Ramdane.