Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-02-22

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #divine
02:47 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
09:40 xstill hm, ty llncs stránky jsou strašně úzký
09:40 mornfall jsou no
09:41 mornfall nezapomeň na to že v tisku to nemá skoro žádný okraje navíc
09:46 mornfall (zase dva čtvercový grafy vedle sebe jsou ještě aspoň na papíře docela čitelný)
09:47 xstill jo to bude potřeba vymyslet, zatím je tam naházím jen tak, pak budu laborovat s velikostí a legendama
09:50 xstill nevíš náhodou kolik má být page limit?
09:51 mornfall Research papers should describe fully developed work and should not exceed 15 pages.
09:52 xstill tak to není úplně málo zase, ne?
09:52 mornfall no, proti 10 IEEE to je +/- stejný, možná míň
10:59 xstill hm, možná máme problém, pthread_barrier nám asertí
11:00 xstill a Milan má v hlavičce napsáno "This test is not complete, but it gives, quite a strong evidence of its correctness."…
11:06 xstill hm, on spíš Milan neumí psát testy, což teda úplně nenapomáhá důvěře v implementaci…
11:10 mornfall zajímavé :)
11:11 xstill tak on inkrementuje neatomickou proměnnou
11:11 xstill bez mutexu
11:11 mornfall a není tam kolem nějaký interrupt_mask?
11:12 xstill není, je to v testech (pthread_barrier.cpp:73
11:12 mornfall aha no ten test asi není moc dobře :-)
11:13 xstill no je celej takovej jetej, ale tohle je celkem jasná chyba
11:13 mornfall no, chyba to nakonec není
11:13 mornfall ale je potřeba si přečíst dokumentaci
11:14 mornfall PTHREAD_BARRIER_SERIAL_THREAD vrátí vždycky jen jedno vlákno
11:14 xstill hm aha
11:15 xstill tak tím hůř potom, protože to může znamena, že je chyba v tí bariéře
11:15 mornfall vždycky to poslední co došlo na tu bariéru
11:15 xstill *tý
11:16 mornfall jak vypadá ten protipříklad?
11:16 xstill serial je 1, má být 2, count je 0
11:16 mornfall ha, je to blbě :-))
11:16 mornfall ty bariéry jsou tam dvě
11:17 xstill no ta druhá je na odejití
11:17 mornfall ano ale každá čeká jen na 2 vlákna a jsou 4... nebo mi něco uniká
11:18 xstill no ta první čeká na 2 vlákna, pak propustí a přičte se to. aha a mezi tím můžou ta další vlákna přeběhnout přes tu stejnou bariéru
11:19 mornfall můžou, ale zase to nemá vracet ten SERIAL_THREAD
11:20 mornfall jo a právě proto to nefunguje
11:20 xstill no běží 4, 2 projdou přes první bariéru, serial loadne proměnnou, další 2 projdou přes první bariéru, seral vlánkno loadne proměnnou, první serial vlákno inkrementuje a uloží, druhé taky -> je to v kelu (řekl bych, že to může nastat)
11:20 mornfall jj
11:21 mornfall chce to ještě jeden mutex
11:21 xstill jo
11:21 mornfall nebo std::atomic když už to je .cpp
11:21 xstill jo to je asi lepší n
11:22 mornfall zase je pravda že dát tam mutex je transparentnější i když škaredý
11:22 mornfall ale ono programování s pthreadama přímo je škaredý vždycky
11:23 mornfall asi bych tam v zájmu jednoduchosti dal ten mutex, ono to jinak asi je i plusminus validní C
11:24 xstill ok
11:29 mornfall jinak jsem tak uvažoval, že kdybychom udělali jinak fronty v shared, mohlo by jít rozumně vyřešit ten overhead v Lake
11:30 mornfall kdyby totiž ta fronta přednostně každýmu vláknu vracela to co do ní to stejný vlákno nacpalo, může být dealokace „cizího“ stavu asi relativně pomalá a nemuselo by to vadit
11:31 mornfall (v podstatě by vlákno mělo dostat „cizí“ stav jen v momentě kdy mu dojdou „vlastní“ ... teda ty který alokovalo)
11:31 mornfall (teoreticky by to taky mohlo trochu pomoct cache lokalitě v generátoru)
11:31 mornfall ono s takovou by to nakonec mohl být i zásobník, kterej se chová asi z tohohle hlediska líp
11:33 mornfall v podstatě by to mohlo fungovat dost stejně jako ty LIFO freelisty co jsou teď v Lake
11:33 mornfall jen to není freelist ale worklist
11:53 xstill ale LIFO asi úplně nechcem kvůli tomu, že pak budou dlouhé protipříklady
11:54 xstill teď teda zatím nevidím, jak by nám to pomohlo s dealokací, ale můžeme se o tom pobavit
11:54 mornfall LIFO + CSDR ;-)
11:54 mornfall no LIFO jako takový asi nijak, ale prioritizace fronty by měla
11:55 xstill jo to jsem ještě pochopil
11:55 xstill že prioritizace front
11:57 mornfall LIFO by pomohlo tomu že když vyrobíš následníky, tak jeden z nich (který je ještě v cache) se hned použije na generování, místo toho aby se vytáhl něakej studenej z konce fronty
11:58 mornfall +j
11:58 mornfall to j je nějaký zrádný :D
12:06 xstill no, mě spíš šlo o to, jak potom udělat tu dealokaci
12:06 mornfall oddělený fast/slow cesty
12:07 mornfall resp. ono to možná bude reálně jedna cesta kódem ale ta atomická instrukce co to bude chránit bude většinou rychlá protože na tu cacheline nikdo jinej nehrabe
23:00 xstill příležitostně pushni ten patch co jsem poslal (včetně toho news) a pak by stálo za to udělat release

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