Community
cancel
Showing results for 
Search instead for 
Did you mean: 
Highlighted
Beginner
5 Views

Please suggest a good book that teaches ...


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.

0 Kudos
0 Replies