On Monday, March 30, 2015 at 10:18:41 AM UTC+2, Tomasz Kaczanowski wrote:
> W dniu 2015-03-28 10:54, M.M. pisze:
>
> >> Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
> >> (bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
> >> inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
> >> do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
> > Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> > wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> > wszystkie pary kodu, który może wykonać się równolegle, były
> > opatrzone semaforami w tej samej kolejności w sensie wykonania i
> > w odwrotnej kolejności (też w sensie wykonania).
>
> Samo opatrzenie semaforami to często za mało by uniknąć dead-locka,
> jeśli sekwencji chronionych jest więcej niż jedna.
No oczywiście. Samo opatrzenie to nawet może spowodować dead-locka.
Chodzi o kolejność. Mamy cokolwiek, semafory, sekcje chronione, itd
blokujące dostęp do zasobów, niech się one nazywają A,B,C.

Jeśli jeden fragment jest opatrzony kolejnością
A
B
kod
B
A

A drugi
B
A
kod
A
B

To może dojść do dead-locka. Gdy kolejność zawsze będzie od A do C, to
nigdy nie dojdzie do dead-locka. Ja wiem że czasami jest tak:

Pierwszy wątek
A
B
kod
B
A

Drugi wątek
B
kod 1
A
kod 2
A
B

Aż prosi się, żeby kod 1 był opatrzony tylko jednym semaforem, ponieważ
można lepiej wykorzystać zasoby systemu. Niestety to gorzi dead-lockiem.
Trzeba w jednym z przypadków zmienić kolejność.

Pozdrawiam


> Dodatkowo dochodzi
> jeszcze dbanie o integralność danych itp rzeczy.
Tutaj zasada też jest prosta. Jeśli na danych pracuję więcej niż jeden
wątek i jeśli przynajmniej jeden wątek może zmodyfikować dane, to
powinno być objęte sekcją krytyczną, semaforem, itd. Czasami stosuje
się rozwiązana lockless, pomimo że wiele wątków pisze pod te same
adresy pamięci - to już w ogóle masakra :)

Pozdrawiam

>
>
> --
> Kaczus
> http://kaczus.ppa.pl/art/liczbyzmiennoprzecinkowe,19
.html