NIAN85: Jasně, ale proč chtít programovat po někom kdo si chodí tvořit ze dřeva ? To nedává smysl ...

SPECZ: Tak kdybych jako fakt musela, ze me by nakonec neco mohlo vypadnout. Uzitecny by byl treba programek, ktery kazdy vstup prevede do depresivni formy a navic uzivatele kreativne popise nadavkami. Pro nektere prispevatele by to mohl byt prima setric mentalni energie.

UNUX: Kravina. Brmlab není omezený jen na programátory.
Je to trochu odvážný, navrhovat jak nabírat členy, od někoho kdo se do brmlabu nikdy nepřišel ani podívat.

PLOSTENKA: Tak kralici nory to jsou a pekne hluboke
do jedne zalezes a nez najdes cestu zpet, 6 mesicu v pr...

> ze instrukce dela tohle a pouze tohle je ta zajimava cast

Souhlasim s tim, ze to je zajimavych je i spousta veci okolo. I kdyz
odmyslis formalni metody a jen si reknes ze udelas nove CPU je tam
dost zajimavych veci na praci. Treba, jak to vubec budes ladit? Jak
pro to budes prekladat kod? A kdyz se rozhodnes to udelat jako
soft-core v nejakem FPGA, uz to neni jen o CPU core ale o celem SoC...

> Je nekde ten verifikovany kompilator k videni, nebo je to inhouse chranene reseni?
Je to k videni, ja uz se dost let veci co nejsou open-source nedotykam
(krom jedne veci, dusledek mladicke nerozvaznosti :-)

Vsechno je to ve fazi vyvoje, je to hodne WIP. Celkovou ideu asi nejlepe
popisuje clanek
Towards a Dynabook for verified VM construction

Co se kodu tyce, je to desnej bordel, dany tim ze vetsinu casu nevime
co delame a pred temi 10 lety jsme byli desne naivni :-)

* Tinyrossa je ten
prekladac, je to brutalne primitivni ve srovnani s modernima prekladacema,
dost veci tomu chybi, POWER backend je hodne pozadu za RISC-V, ostatni
architektury jsou jen experimenty. Nicmene kod to produkuje a je mozne
ho pustit jak v simulatorech (gem5, qemu) tak na FPGA soft-cores
nebo realnem kremiku (SiFive U540, StarFive JH7110, PPC e500, POWER).
Ta formalni stranka jeste neni zaintegrovana, najdes ji v branchi
MoreVMs24. Nejake trivialni priklady co to umi jsou
TRMoreVMs24.class.st.

* Arch je knihovna
co resi instruction encoding a assembler/dissasembler pro ruzne ISA.
Funguje to, umi to dost, ale je treba to cele predelat. Akorat zatim
nevim jak presne :-)

* MachineArithmetic
je ta "matematika" co je za tim. To je hlavne prace kolegy, on je
matematik, ja jsem jen obycejny inzenyr, takze tam delam jen tu
nejspodnejsi vrstvu kolem interfacu k Z3.

Pak samozrejme mame spousty jinych veci okolo, neco jsou kravinky
na odreagovani kdyz se nam zavari mozek, neco je prace na externich projektech
kam prispivame vecma co potrebujeme (GDB, OMR, gem5). Co se tyce
semantiky ISA idea je
Sail->JIB->MachineArithmetic semantic core. To je zatim v plenkach a bude
to dost zajimave, protoze treba semantika ARMv8 ISA vycucla z ASL a natazena
do Coqu (nebo Isabell) zabira ~500GB RAM, takze to uz chce lepsi pocitac
a slusnej GC.

JANFROG: A nechces prist niekedy na matecko pokecat?:)

JANFROG: Multidimenzionalni kralici nory? Ale beze vseho!

Formalni verifikace, ze instrukce dela tohle a pouze tohle je ta zajimava cast. Jestli se v Racketovem zdrojaku nadefinuje, ze ma registr 8, 64 nebo 19 bitu je vlastne nezajimavy implementacni detail, vygenerovany emulator vygenerovaneho bytecode si s tim poradi. Podobne pro jine napady okolo ISA. A jak se rika pri navrhu cehokoliv sloziteho od piky - cesta je cil.

Je nekde ten verifikovany kompilator k videni, nebo je to inhouse chranene reseni?

RAINBOF: Teda kluci a holky, fandim vam, tyhle veci jsou super zajimavy! (nebo mi to alespon tak prijde)

Ale prijde mi, ze nemate uplne predstavu jak moc velky sousto jste si ukousli :-) Ja motam kolem RISC-V temer od jeho pocatku (jsem clenem J-ext WG, kde se mimo jine resi i ten zminovany pointer masking / pointer tagging). Jen to "pres instrukcni sadu": myslim ze na RISC-V summitu 2018 v Santa Clara Andrew Waterman rikal, ze puvodne chtel jen navrhnout jednoduchou ISA pro vyuku, myslel ze to spichne pred prazdniny za 2-3tydny a nakonec na tom delal Krsteho team 3 roky a to byla jen tak zakladni sada (zadne bitove manipulace, zadne vektory, crypto, apod). "The RISC-V Instruction Set Manual Volume I: Unprivileged ISA" je dobre si precist, je tam dost poznamek o tom proc veci jsou udelane tak a ne jinak.

Ted delam na projektu ktery se toci kolem formalne verifikovaneho prekladace a je to naproste silenstvi. Kolega na tom projektu dela 10 let, ja 5 let, je to nas full time job a stejne to neumi vic nez trivialni priklady a to (zatim) bez verifikace vygenerovaneho strojoveho kodu. Uz jen jak formalizovat semantiku ISA je orisek. Semantiku instrukci jeste jaks taks (i kdyz takove load/store instrukce jsou super komplikovane), horsi je to s memory modelem.

Ale jak rikam, je to naprosto fascinujici oblast.

brmlabi skupina ktera se pokousi napsat vlastni bezpecny procesor.
Jitsi Meet
https://meet.jit.si/ledum-wg-meetup

Navrhujeme vlastni provak ... tedy ... zrovna ted si navzajem davame prednasky o tom, co nekdo neumi, abychom si synchronizovali znalosti.
4:51 PM
ihaveyourllama: navrh vlastniho procaku od uplnych teoretickych zakladu (VHDL scitacky..), pres navrh registru/pameti, pres instrukcni sadu (jak kodovat instrukce v binarce)... az po prakticke vyuziti pro pravdepodobne pomale, ale formalne verifikovane(=bezpecne?) vypocty
4:52 PM ihaveyourllama: zatim vlastne nevime jak to bude ve finale vypadat, zjistujeme a ucime se navzajem za pochodu ruzne lowlevel veci
4:53 PM
lhc ihaveyourllama: S tim, ze tam nebude normani OS, ale bude rozsekany na ruzne casti, z nihz zadna nebude mit kompletni opravneni delat vsechno a budou od sebe oddelene kremikem. +k tomu tagovani pointeru a tak, aby se nestavaly klasicke problemy programovani v C, jako preteceni bufferu a tak ...

XCIDER: z něčeho takovyho už jsem kuchnul i 550mAh ...

x.com
https://x.com/SpeczG/status/1645340216482308096?t=hRav51dGTzgJAIvy_D0ASA&s=19