-
X-Received: by 10.140.41.104 with SMTP id y95mr462307qgy.7.1427711063859; Mon, 30 Mar
2015 03:24:23 -0700 (PDT)
X-Received: by 10.140.41.104 with SMTP id y95mr462307qgy.7.1427711063859; Mon, 30 Mar
2015 03:24:23 -0700 (PDT)
Path: news-archive.icm.edu.pl!agh.edu.pl!news.agh.edu.pl!news.cyf-kr.edu.pl!news.nask
.pl!news.nask.org.pl!goblin2!goblin.stu.neva.ru!newsfeed.xs4all.nl!newsfeed3a.n
ews.xs4all.nl!xs4all!newspeer1.nac.net!border2.nntp.dca1.giganews.com!nntp.giga
news.com!z60no566165qgd.0!news-out.google.com!q90ni547qgd.1!nntp.google.com!q10
7no566159qgd.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-m
ail
Newsgroups: pl.comp.programming
Date: Mon, 30 Mar 2015 03:24:23 -0700 (PDT)
In-Reply-To: <551906e0$0$2198$65785112@news.neostrada.pl>
Complaints-To: g...@g...com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=178.36.122.220;
posting-account=xjvq9QoAAAATMPC2X3btlHd_LkaJo_rj
NNTP-Posting-Host: 178.36.122.220
References: <4...@g...com>
<d...@g...com>
<meti4e$osd$1@srv.chmurka.net>
<f...@g...com>
<mevfpd$gpa$1@srv.chmurka.net>
<e...@g...com>
<mf1tnf$d48$1@srv.chmurka.net>
<d...@g...com>
<e...@g...com>
<f...@g...com>
<b...@g...com>
<4...@g...com>
<f...@g...com>
<8...@g...com>
<551906e0$0$2198$65785112@news.neostrada.pl>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <d...@g...com>
Subject: Re: poprawność algorytmu
From: "M.M." <m...@g...com>
Injection-Date: Mon, 30 Mar 2015 10:24:23 +0000
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable
Lines: 83
Xref: news-archive.icm.edu.pl pl.comp.programming:207713
[ ukryj nagłówki ]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
Następne wpisy z tego wątku
- 30.03.15 20:08 Andrzej Jarzabek
- 31.03.15 02:07 Roman W
- 31.03.15 09:05 slawek
- 31.03.15 09:56 Maciej Sobczak
- 31.03.15 12:20 g...@g...com
- 31.03.15 14:48 M.M.
- 31.03.15 16:39 g...@g...com
- 31.03.15 19:08 slawek
- 31.03.15 19:29 M.M.
- 31.03.15 19:43 M.M.
- 31.03.15 19:49 g...@g...com
- 31.03.15 19:59 slawek
- 31.03.15 20:10 slawek
- 31.03.15 20:34 g...@g...com
- 31.03.15 21:01 M.M.
Najnowsze wątki z tej grupy
- 7. Raport Totaliztyczny: Sprawa Qt Group wer. 424
- TCL - problem z escape ostatniego \ w nawiasach {}
- Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- testy-wyd-sort - Podsumowanie
- Tworzenie Programów Nieuprzywilejowanych Opartych Na Wtyczkach
- Do czego nadaje się QDockWidget z bibl. Qt?
- Bibl. Qt jest sztucznie ograniczona - jest nieprzydatna do celów komercyjnych
- Co sciaga kretynow
- AEiC 2024 - Ada-Europe conference - Deadlines Approaching
- Jakie są dobre zasady programowania programów opartych na wtyczkach?
- sprawdzanie słów kluczowych dot. zła
- Re: W czym sie teraz pisze programy??
- Re: (PDF) Surgical Pathology of Non-neoplastic Gastrointestinal Diseases by Lizhi Zhang
- CfC 28th Ada-Europe Int. Conf. Reliable Software Technologies
- Młodzi programiści i tajna policja
Najnowsze wątki
- 2024-11-29 Dławik CM
- 2024-11-29 [OT] Lewe oprogramowanie
- 2024-11-29 Błonie => Sales Specialist <=
- 2024-11-29 Warszawa => IT Expert (Network Systems area) <=
- 2024-11-29 Warszawa => Ekspert IT (obszar systemów sieciowych) <=
- 2024-11-29 Warszawa => Head of International Freight Forwarding Department <=
- 2024-11-29 Białystok => Inżynier Serwisu Sprzętu Medycznego <=
- 2024-11-29 Pómpy ciepła darmo rozdajoo
- 2024-11-29 Białystok => Application Security Engineer <=
- 2024-11-29 Białystok => Programista Full Stack (.Net Core) <=
- 2024-11-29 Gdańsk => Software .Net Developer <=
- 2024-11-29 Wrocław => Key Account Manager <=
- 2024-11-29 Gdańsk => Specjalista ds. Sprzedaży <=
- 2024-11-29 Chrzanów => Specjalista ds. public relations <=
- 2024-11-27 Re: UseGalileo -- PRODUKTY I APLIKACJE UŻYWAJĄ JUŻ DZIŚ SYSTEMU GALILEO