Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-11-29

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
07:44 xstill pro velký úspěch divine vygeneroval 242M stavů a zasegvil
09:23 xstill jinak s tím relaxed, ten momotonic flag funguje, ale musím počtat až pro tu lokaci v žádném store bufferu žádný nebude. Jinak by totiž existoval protipříklad proti TSO (on relaxed s TSO je reálně acq_rel), ten protipříklad (všechno relaxed): vlákno t1 zapíše x = 1, y = 1; t2 přečte y, zapíše výsledek do z; t3 přečte z = 1, x = 0, takže vidí efekt zápisů z vlákna 1 v opačné
09:23 xstill m pořadí. Takže z toho mi plyne, že ...
09:23 xstill ... všechny atomické operace budou mít ve store bufferu monotonic flag, pokud chci provést atomickou operaci jinou než musím počkat, až na její adresu nebude žádný monotonic. Ovšem taky z toho plyne, že v MEMICSu mám blbě atomické (SC) loady, SC operace myslím musí mít SC flag kterej nesmí být u žádné adresy v žádném bufferu aby se mohli spustit (to mi vychází z definice). Otá
09:23 xstill zka pak je jestli SC store má jít do bufferu, ...
09:24 xstill ... asi jo, je pořád možný, že někdo udělá ne-SC load na tu adresu.
09:24 xstill (sorry za to dělení, zdá se že irrsi se naučila dělit správy a dělá to jinak než ten skript kterej jsem si na to přidal :-D)
10:03 xstill mornfall: jinak by se dost hodil nějaký __divine_assume, navrhoval bych aby se to chovalo tak, vyhodnocení __divine_assume( false ) způsobí, že stav vůbec nebude vyprodukován. Kvůli korektnosti je potřeba aby se to k redukci chovalo stejně jako __divine_interrupt_mask, tj. při naražení na assume  pokud už bylo něco vidětelného před tím se vygeneruje stav (než se jde na ten assume). Co s
10:03 xstill i o tom myslíš. Ono totiž potom by se dalo ...
10:03 xstill ... dělat "čekání" pod maskou, což je výrazně příjemnější pro weakmem (a asi i pro pthready nakonec), například TSO a PSO by se mohli lišit jen tím jak mají napsaný flusher thread.
10:33 mornfall ten assume mi zatím není jasnej
10:34 mornfall hm, je to dost neintuitivní
10:35 xstill co je neuntuitivní, assume nebo memory modely?
10:35 mornfall assume
10:35 mornfall resp. to že vygeneruje ten stav před
10:36 mornfall a hlavně že by se to mělo stát aj pod maskou?
10:36 mornfall aha ne
10:37 mornfall ne to nedává smysl, assume nesmí vygenerovat nic
10:38 xstill motivace: prostě místo while ( !pred ) { breakmask; } chci psát assume( pred );, pod maskou nemůže vynutit stav; mě šlo o to aby ten assume nenechal zmizet nějakiu viditelnou akci. I když teď si skoro myslím, že pokud po té akci nevyhnutelně (to jest bez interruptu) následuje assume false, tak se to může zaříznout a ta akce může zmizet
10:38 mornfall no to musí
10:38 mornfall (zmizet tu akci)
10:38 xstill nemusela by (pokud není pod mazkou)
10:38 xstill *maskou
10:38 xstill fuj
10:39 mornfall jo, pod maskou
10:39 mornfall to by nadělalo parádní bordel totiž
10:39 xstill pokud je assume( false ) pod maskou, tak musí zmizet celá ta maska
10:39 mornfall bys mohl vidět půlku maskovaný sekce
10:40 mornfall a do atomický sekce nesmíš ani vlézt pokud máš nějakou necommitnutou viditelnou akci
10:40 xstill jasný, mě šlo o ty nemaskovaný
10:41 mornfall myslím že v nemaskovaný to není potřeba řešit
10:41 mornfall aby se to rozbilo, musel by ten assume záviset na něčem co provede jinej thread
10:42 mornfall a to se musí commitnout před odpovídajícím loadem
10:42 xstill ono totiž pak by se hezky implementovaly ty věci ve weakmem, stačilo by v podstatě něco jako assume( !monotonic_flag_on_location( x ) ); load x v implementaci třeba monotonic (relaxed) loadu
10:43 xstill (pokud si nečetl to o těch atomikách na začátku tak si to posím ještě přečti)
10:43 mornfall jo četl ale ještě jsem se z toho nevysekal
10:43 mornfall nevim co je z
10:44 mornfall aha vim, jen neumim číst
10:44 mornfall no ale to je úplně dovolený (pod relaxed)
10:44 mornfall protože to je jiná lokace
10:47 xstill jo, jenže pokud chceme simuvat TSO tak nemůžem přehazovat store (tj. TSO + relaxed = acqrel řekl bych). Ale teď si myslím, že dokážu poměrně snadno (s assume) implementovat i víc relaxovanej model
10:47 mornfall nojo, tso říká že relaxed neexistuje :-)
10:47 mornfall teda ten relaxed kterej je nadefinovanej v langrefu aspoň
10:49 mornfall (celý bych to řešil implementací těch modelů z langrefu a když si člověk řekne o tso tak se to co je slabší příslušně upgraduje)
10:52 xstill on je tam reálně jen rozdíl v tom, jak se můžou flushovat ty buffery, ne? Pro úplně relaxované můžu vše za nejstarším release flushovat v libovolném pořadí (až na věci co jdou na stejnou lokaci), pro TSO je to fifo. A pak si můžu klidně pořád čekat až to "dojde" do paměti v tom relaxed loadu
10:53 mornfall jo asi jo
15:07 xstill mornfall: prosímtě, jak chápeš to jak popisují fence v http://llvm.org/docs/Atomics.html#atomic-instructions ? já bych očekával, že ten fence bude před loadem a za store, takhle moc nechápu jak to má fungovat…
15:20 mornfall fence se použije asi spíš když máš nějakých N operací které se mezi sebou můžou proložit jak chcou a pak N+první která musí být vidět až po těch N
21:24 ilbot3 joined #divine
21:24 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
22:42 ilbot3 joined #divine
22:42 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary