Prev: From typeless language to C/C++
Next: Parallel Compression 1.0 ...
From: aminer on 30 Mar 2010 18:09

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 constante


and


M(P) + M(R) + M(S) is too equal to a constante


Note also that vector f * M0 (initial marking) = 0


So it follows - from the equations - that since
M(P) + M(R) + M(S) = C1 , it means that
M(P) <= C1 and M(R) <= 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 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 , you can have a deadlock in this system.


That's what we call a 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.


From: Ian Collins on 30 Mar 2010 18:12
On 03/31/10 11:09 AM, aminer wrote:

Please don't multi-post.

--
Ian Collins
From: aminer on 30 Mar 2010 18:23

I wrote:

>[..]
> 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 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 , you can have a deadlock in this system.
>
> That's what we call a 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 - ?


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 ?



Sincerely,
Amine Moulay Ramdane.





 | 
Pages: 1
Prev: From typeless language to C/C++
Next: Parallel Compression 1.0 ...