Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-07-04

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #divine
01:47 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
07:15 xstill nojo, já měl bug v těch store bufferech (load nedělal interrupt), i když teda ještě se budu muset zamyslet proč to byl problém…
07:19 xstill ono totiž úplně stačí aby všechno zůstalo ve store bufferu a tím, že každý vlákno čte flag toho druhého, tak tam uvidí false a pustí se do kritické sekce
07:20 mornfall nojo :)
08:18 xstill veselý, ten peterson má celkem přes 3M stavů
08:19 xstill (tu chybu jde ale najít poměrně rychle)
09:01 xstill mornfall: poslal jsem patche co opravují pár věcí v userspace, ten validate a přidávají do examples to co jsem zatím udělal na těch store bufferech, u mě to prošlo testama (až na stacksave)
09:10 xstill mornfall: k čemu je to ID v tom lartovém pass-u?
09:49 xstill hm, blbý je že vůbec netuším jak anotovat ty funkce, clang zdá se neumí žádný atribut který by se na to dal zneužít :-/
10:08 xstill aha tak přece
12:20 xstill no vida, tak už umím poznat anotovaný funkce
18:44 xstill mornfall: nemáš náhodou po ruce build llvm s assertama? anebo nevíš proč by dump na bitcast mezi dvěma pointrama mohl segvit?
19:07 mornfall je ta instrukce OK? musí mít všechny operandy definovaný
19:09 mornfall build nemám, ale možná bych ho mohl stejně vyrobit
19:10 xstill typ i operand se dumpnout dá (operand je původem parametr z loadu)
19:12 mornfall to je trochu divný no
19:14 xstill ovšem on to nějak zmrší IRBuilder, když tu instrukci nejdřív vytvořím tak jí ještě dumpnout jde, až když pak udělám builder.Insert tak to segví
19:15 xstill hm, a podle valgrindu to hrabe na 0x18 někde v llvm::DebugLoc::getAsMDNode
19:16 mornfall dobrý no
19:17 xstill radost no…
19:20 xstill ani nevím co to tam tvoří s těma metadatama
19:20 xstill zajímavý na tom je, že když ten bitcast vynechám tak ostatí instrukce se mi tam naskládají v pohodě (ale nesedí to typově)
19:30 xstill aha, to je trapný, já měl blbej kontext
19:32 xstill takže když jsem typ toho bitcastu vytvořil ve správným kontextu tak to najednou funguje
19:32 mornfall :-)
19:32 xstill co je to vlastně za krám ten kontext?
19:34 xstill aha to si nějak drží pointry na struktury s typama a tak, jo? Takže když vytvořím 2x typ (nebo ho vytáhnu z instrukce) tak bude mít stejnej pointer, pokud je to všechno ve stejným kontextu?
19:56 xstill ha, už to nahrazu loady i story, dokonce tak, že ten bitcode se načte do divine :-)
19:56 xstill s/nahrazu/nahrazuje/
19:57 xstill hm, ale že by to fungovalo se říct zase nedá, iniciální stav se nějak nechce vygenerovat
19:58 mornfall že zrovna iniciální
19:58 xstill hm, machine.h: 326: assertion `segment + segshift <= int( 1u << Pointer::segmentSize ) - 1' failed; got [65536] > [65535] instead
19:58 xstill asi bude něco špatně :-D
19:58 mornfall řekl bych že se to lehce zacyklilo
19:59 mornfall určitě je to dobře anotovaný a přeskakuje se to?
19:59 mornfall (teda ty fce co to implementujou)
19:59 mornfall (a všechny který se z toho volaj... a tak)
19:59 mornfall (to by mohl být trochu problém co? :\)
20:00 xstill jo to je v pořádku zrovna
20:00 mornfall já ten kód teda nevidim tak nevím co může volat, ale aby to fungovalo tak nesmí asi vůbec nic (určitě nic z STL)
20:00 xstill jakože momentálně se anotace propagují na všechno co se volá z anotovaných, což zatím nevadí protože ty anotovaný funkce skoro nic nevolaj (co není intrinsik)
20:01 mornfall ok
20:01 xstill já si to jdu prokrokovat bez redukcí tam to iniciální stav vygeneruje
20:01 mornfall nicméně na iniciální stav nic z toho nemůže mít vliv
20:01 mornfall ten se generuje dost staticky
20:02 mornfall spíš nefunguje generování jeho následníků
20:02 xstill jo to je možný, simulate generuje rovnou i následníky aby věděl kolik je
20:08 xstill nojo, nevím proč na tom teda interpretr cyklí, ale ono dělat store před tím, než se pustí globální konstruktory není moc dobré, protože nejsou naalokované buffery
20:09 xstill hm, i když to by nemusel být až takový problém asi
20:20 xstill a to, že se dělá store na adresu 0 se mi taky moc nelíbí
20:38 xstill hm, tak přece je to blbě
20:39 xstill protože memmove, ono je schovaný za intrinsikem takže jsem si ho nevšiml a potom volá store buffer zase :-/
20:39 xstill takže nesmím asi fakt nic používat
20:47 xstill do háje, ono přiřazení struktury vygeneruje memcopy
20:48 xstill já snad budu muset udělat to, že při vstupu do store/load nastavím flag a další store/load budou pak psát přímo pokud ten flag uviděj, pak by mělo stačit mít označkovaný jen vstupní funkce teoreticky
20:59 xstill nojo to funguje, ale pěkné to moc není
21:00 xstill teda funguje… pokročí dál než před tím
21:01 xstill mornfall:   __storeBuffers = @(89:0| { @(0:0| @(1:0| { 0 })), 0 })
21:01 xstill zdá se mi to, nebo se tomu modelu podařilo něco uložit na NULL?
21:08 xstill hm, do háje, když v tom store bufferu budou ukazatele na stack a přežijou konec funkce tak to asi udělá nějakej bordel, co?
21:11 xstill mornfall: ono to skoro vypadá, jako by první alloca měla adresu 0:0. I když to by potom asi znamenalo, že je to heap adresa, ne?
21:25 xstill jo no, tak už ukládám na invalid pointer :-/
21:34 xstill asi budem muset přidat nějakej kód před ret, kterej invaliduje položky co jsou na stacku, ale to bude možná docela bolet
21:37 xstill (jakože položky který budou na konci funkce ve stacku se zruší bez náhrady, mimo pořadí, to asi bude korektní, protože kdyby někdo měl pointer na stack, tak, že by se v reálu mohl store projevit až tam bude jiná funkce, tak stejně asi chce vědět, že ten load je někam kam neměl, což bude, divine by měl nahlásit potom invalid load)

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