Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-10-04

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

All times shown according to UTC.

Time Nick Message
03:53 mornfall joined #divine
10:06 mornfall yaqwsx: já si myslim žes tam měl LLVM_LIBRARY_DIRS z předchozí konfigurace, pak jsi přidal/změnil llvm-config a cmake ty proměnný neupdatuje (to co jsem říkal ad smazat CMakeCache.txt nebo ccmake -> d)
10:52 yaqwsx joined #divine
11:15 yaqwsx joined #divine
11:39 xstill yaqwsx: jak to vypadá s tím sw-compem, má symdivine šanci?
11:58 yaqwsx Ještě nevím. Chtěl jsem si SymDivine nechat project tím benchmarkem, kterým mají ve Formele, ale kluk, který to má na storosti je teď dva týdny v Německu.
11:59 yaqwsx Jinak dobrá zpráva - v concurrency nechtějí protipříklady (protože nemají vhodný formalismus na jejich reprezentaci)
12:01 xstill a nikdo jiný tam s tím neumí? takže nebudete muset řešit protipříklady? to by bylo fajn :-) nebo chcete soutěžit i jinde?
12:02 yaqwsx Prý nikdo jiný. Ale dneska v noci se měl vrátit, tak snad se zítra dozvím více.
12:02 yaqwsx BTW: Po úpravě toho Divinu mi z něj nevypadne binárka divine, ale binárku runner - je to v pořádku?
12:03 xstill co? ne měl bys mít tool/divine
12:03 xstill když pustíš make divine, jen make možná někde zdechne
12:03 yaqwsx Teď nás v SV compu asi nejvíce pálí malloc - ale asi už mám nemyšlené, jak ho pro účely SV compu vyřešit.
12:03 xstill teda tools/divine
12:04 xstill jo? co s ním uděláš?
12:04 yaqwsx Hm, když jsem znovu zavolal make, tak to něco slinkovalo a objevil se tam. Zvláštní...
12:21 yaqwsx Prošel jsem příklady z SV compu a vždy se malloc používá místo pole, vždy se alokuje pouze jednou a nikdy se nefreeuje. Takže kdykoliv bude proveden malloc, podívá se na následující bitcastovou isntrukci a dle ní zkonstruuji pole na samostatném zásobníku, který nechám žít až do konce aplikace.
12:23 yaqwsx_cz joined #divine
12:28 yaqwsx_cz Z pohledu SV compu by to mělo být korektní (a korektní v případě, kdy nehlídám a paměť a nikdy ji nefreeuji)
12:28 xstill aha, pak moc nechápu proč tam ten malloc vůbec mají…
12:29 xstill je to dynamicky velké, to co alokují?
12:36 yaqwsx_cz Není
12:36 yaqwsx_cz Podle mě je tam jenom na opruz :D
12:37 xstill mornfall: tau komprese skryje i volání funkce, pokud ta funkce nehrabe na nic viditelného a neobsahuje cyklus ani rekurzi?
12:37 xstill hm, to pak moc nechápu smysl toho mallocu, dalo by se to nahradit i globální proměnnou klidně
12:38 xstill to mě příjde jako "zkusíme odfiltrovat ty, co ani nechápou jak ten jejich tool funguje, nebo co je malloc"
12:38 yaqwsx_cz Jako ano, dalo. Pokud by nedalo, tak nemáme šanci (a asi ani pořádně nikdo další na světě)
12:39 xstill a jak moc je tam vstupů?
12:40 yaqwsx_cz Zpravdila pár (copak, přemýšlíš nad klasickým Divinem?)
12:41 xstill tak přemýšlím, ale muselo by to jít v podstatě bez úprav :-D, jako pár proměnných? A jak velkých?
12:41 yaqwsx_cz http://ben11.fi.muni.cz:3000/results/byCategory/41?svcomp_tools[]=31&symbiotic_tools[]=265
12:41 yaqwsx_cz Všechno zpravidla 32 bit
12:41 yaqwsx_cz https://github.com/dbeyer/sv-benchmarks/tree/master/c/pthread
12:46 xstill koukám že v svcompu malloc neselhává, on je fakt na nic
13:05 xstill mě ten svcomp příjde docela k smíchu, minimálně ty pthread příklady musí jít umlátit exlicitní enumerací množin možných hodnot pomocí intervalů
13:05 mornfall xstill: jo, skryje
13:05 xstill ok
13:05 mornfall mi*, přijde* :P
13:06 xstill nojo
13:07 mornfall a jako jo, svcomp
13:08 mornfall do toho bych šel až s abstrakcema
13:08 mornfall a stejně to bude hlavně opruz
13:10 xstill taky mám ten pocit, že hlavní efekt je že je to opruz, a ne že by to bylo těžký
13:12 xstill teda z toho mála co jsem viděl
13:36 zbeasnyy joined #divine
16:17 yaqwsx_cz joined #divine
16:19 yaqwsx_cz Je pravda, že ty ostatní kategorie jsou zajímavější (leč pro SymDivine celkem obtížné)
16:20 yaqwsx_cz Ještě jsem na Sv compu moc nepochopil význam pre-submit deadlinu.
16:34 yaqwsx_cz Ha, teď jsem narazil na příklad, kde má malloc alespoň trochu smysl...
16:37 xstill a co dělá?
16:38 yaqwsx_cz Globální pointer, jedno vlákno udělá malloc, druhé do nalokované paměti zapíše.
16:41 xstill aha, pořád nic moc :-D
16:42 xstill proč vlastně neumíte malloc? je nějaký důvod proč je to problém i pokud je velikost explicitní?
16:43 yaqwsx_cz Neumíme ho, protože neumíme pracovat s blobem paměti - potřebujeme ji reprezentovat jako pole stejných prvků o známé velikosti.
16:44 yaqwsx_cz + všechno uvažujeme jako stack.
16:45 yaqwsx_cz Ale pro účely SV compu se to dá obejít zjištěním velikosti prvku z bitcastu a umístěním na samostatný zásobník.
16:45 yaqwsx_cz Doufám, že mě nepřekvapí nějaká záludnost s pointery.
16:53 xstill aha, ono možná by mohlo jít ten malloc vždycky vyřešit tak, že by to vytvoří nový stack pro každé volání, tam se pustí alloca s příslušným typem z bitcastu (alloca může alokovat i dynamicky mnoho paměni) a free ten stack zruší, pokud teda dokážete takové věci se stacky zvládnout
17:04 mornfall xstill: jo to je to stejný jako umět malloc
17:04 mornfall nepřijde mi že by to čemukoliv pomohlo :-)
17:05 xstill no to je, to vím
17:05 mornfall to má tak trochu zřejmej problém s nekonečně mnoha zásobníkama
17:06 mornfall (ne že by pthread_create v cyklu podle vstupu nedělalo to stejný)
17:06 xstill no, divine taky nezvládne alokaci v cyklu, to není nic extra specielního
17:07 mornfall divine žádný cykly podle vstupu neřeší
17:07 xstill ale pořád může mít nekonečný cyklus s mallockem
17:08 xstill pokud teda ten ukazatel neuložíš, tak to samozřejmě půjde, ale když to přidáš do linkedlistu tak to časem padne na moc velký stav
17:08 mornfall to je ale jinej problém
17:08 mornfall pro symdivine jsou proměnný 0-2^64 raison d'être
17:09 * xstill neumí francouzky nebo co to je
17:09 mornfall důvod bytí (google by pomohl)
17:10 xstill stejně to nechápu
17:10 mornfall no, symdivine existuje proto abys mohl mít nespecifikovaný vstup
17:10 mornfall a jeho užitečnost se odvíjí od toho co s takovým vstupem můžeš udělat
17:11 xstill jo tak, jasně ale řešení mallocu podle symbolické hodnoty je úplně jiný problém a musí se řešit jinak
17:12 mornfall tak to vychází z toho že mi přijde svcomp jako ztráta času, takže dohackovávat jednu po druhé věci který stejně k ničemu jinýmu nebudou je takový mrzutý
17:13 mornfall hlavně když máme docela dobrou představu jako 'explicitní' nedostatky v symdivine vyřešit paušálně
17:13 mornfall jak*
17:15 mornfall jakože nový zásobníky neřeší žádnej novej problém, je to jen hack jak mít polovičatou podporu malloc-u, která navíc funguje jen pro velmi omezené použítí malloc-u (svcomp)
17:16 mornfall to má zase pak smysl (pokud je svcomp priorita) udělat minimální nutnou změnu, tzn. ohackovat to tak aby to fungovalo přesně pro ty 2 případy co se v svcomp objeví
17:16 xstill jenže svcomp musíš brát jako reklamu, jinak nemá smysl. Pro divine je to reklama asi dost zbytečná, pro symdivine možná ne
17:17 mornfall reklama pro něco co sotva funguje je taky zbytečná :P zejména pokud je na výběr mezi reklamou a řešením toho aby to fungovalo líp
17:18 mornfall navíc to je reklama dost omezená pokud hraješ jen jednu okrajovou kategorii
17:19 mornfall když budem makat, za rok nebo dva si můžem troufnout na cpachecker
17:21 xstill jakože s integrací symdivine makat?
17:44 mornfall makat jakože !(flákat se)
18:01 yaqwsx joined #divine
18:04 yaqwsx Sv comp mi přijde v symbolickém světě jako hodně omílaná a osobně v ní vidím možnost ověření si, jak na tom oproti ostatním jsme. A to, že je třeba něco ohackovat cestou nejmenšího odporu, vidím teď jako nutné zlo.
18:11 xstill mornfall: btw, ta tvoje optimalizace weak memory transformace kvůli tau nebude fungovat s PSO (zapsat do lokáně dostupné paměti; zveřejnit paměť; flushnout buffer v opačném pořadí -- tohle není možné). Ne že by to teď vadilo, jen kdyby náhodou jsme někdy chtěli PSO…
18:32 xstill mornfall: kdy budeš mít ten interpreter?
18:36 xstill ten současnej totiž segví i když nepoužiju explicitně zádné atomické věci (asi jsou v knihovně)
18:39 xstill a už mě to začíná brzdit, protože jsem pod dojmem toho, že to bude začal psát transformace do portovanýho lartu, takže je teď nemám jak zkoušet
18:43 mornfall je to v next-u, ale nemá se to moc rádo s std::string (asi; v fs-* to hlásí uninitialised value, mám pocit že už to někdy bylo ale nevim co přesně)
18:43 mornfall jo a není tam arithmetic with overflow, protože to žádnej test asi nepoužívá
18:43 mornfall (počítám že změna v clang-u)
18:44 mornfall jsem zjistil že většina jich tam nebyla ani předtím
18:45 xstill arithmetic with overflow je asi další věc co případně můžeme řešit lartem, ne?
18:45 mornfall teoreticky, ale bude to mít dopad na codegen
18:45 xstill ten std::strign byly rozhašený pointr flagy někde
18:46 xstill jo, ted dopad na codegen (jestli myslíš generování nativního kódu z výsledku compile) mě už taky napad, tenhle lowering by asi mohl běžet až při loadu modulu do divine (bude rychlej)
18:48 mornfall druhá možnost že se to naučil IntrinsicLowering kterej už používáme
18:48 mornfall (llvm/CodeGen/IntrinsicLowering.h)
18:48 mornfall jo a std_string.sh mi teda prochází, projevuje se to jen v fs-*
18:50 mornfall jestli to nebylo s tím (ne)usekáváním pointrů
18:51 mornfall ale asi ani ne, to vypadá dost stejně jako ta výsledná verze z minula
19:02 xstill nezdá se mi, že by lowering uměl with overflow, asi se prostě negenerují (nevíš odkud šly?)
19:03 mornfall nějaký indexace pole tuším
19:09 yaqwsx joined #divine
19:18 xstill hm, mám dva modely, která se liší jen na základě transformace co jsem si myslel, že je ekvivalentní pod tau+, a maj různej počet stavů… to bude dobrá detektivka zase jednou
19:18 mornfall jak moc velký jsou?
19:19 xstill 779 a 862 stavů
19:19 mornfall nj, to je docela na hranici
19:19 xstill ale asi je můžu zmenšit
19:27 xstill hm, dokonce 2 takový transformace mám :-/
19:30 yaqwsx joined #divine
19:31 xstill hm, 140 stavů, pořád trochu moc na to aby se mi to chtělo krokovat…
19:33 xstill možná draw, ale tam to zas vypadá dost zásadně jinak
19:41 xstill a graphviz stejně draw -l nedal
19:41 xstill achjo
20:16 yaqwsx joined #divine

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