Please suggest a good book that teaches ...

[aminer10]

Srinivas Nayak wrote in comp.programming.threads:
>Dear All,
>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.
>4. synchronization.
>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.
>17. lock-freedom.
>18. wait-freedom.
>19. deadlock-freedom.
>20. starvation-freedom.
>21. livelock-freedom.
>22. obstruction-freedom.
>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
>correct.
>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.
>With regards,
>Srinivas Nayak

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

and

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
structuraly bounded.

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
'good patterns'.

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
sharing etc.

Do you understand why I and others follow also good patterns
- that look like theorems - ?

Think about it...

Take care...

Sincerely,
Amine Moulay Ramdane.