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.