haskell @ hackday

[Yakov ZAYTSEV]

вдруг кому-то будет нехер делать целых два выха
может присоединицо ко мне
(правда я не понял, как там это все будет апрувицо)

http://spb.hackday.ru/projects.html#project29

DSP kernel can be generated automagically from the specification. Using superoptimization techniques to compile kernels it would be possible to avoid costly manual assembler coding.

To bring the idea to life for the DFT we are working on optimizing assembler code generator for ADSP-TS201S processor for genfft compiler from the FFTW suite.

As of today we have patch for the genfft which makes it output Haskell program This program is compiled with the GHC in turn. When run, program outputs (Tiger-)SHARC assembly listing to be fed VisualDSP assembler.

Incomplete list of ideas for this hackathon
- to use Coq proof assistant to rewrite some of the Haskell code in.
- to prototype Denali approach to superoptimization to some extent (see http://people.csail.mit.edu/randall/papers/abstracts/denali.html)
- new ideas are welcome ;-)

I've started this project.

You can reach me at ya...@yakov.cc

PS
Required prerequisites include good practical exposure of Haskell programming.
Concerning Coq idea you are expected to have basic understanding of the system and willingness to learn.

[Maxim Taldykin]

Я вот сейчас читаю про denali, идея-то интересная, но я сомневаюсь,
что произвольным количеством программистов можно сделать theorem
prover за 12 часов.
Или предполагается взять готовый?
Как-то не понятно, прототип чего (и в каком объёме) должен получиться на выходе.

2009/11/22 Yakov ZAYTSEV <iak...@gmail.com>:

[Yakov ZAYTSEV]

если поразбираемся с листком бумаги и ручкой, то хорошо. если выйдет что-то написать, то вообще здорово.

нет установки сделать прототип (у меня лично).
я скромно хочу поработать над проектом ;-)

не, theorem prover там не нужен IIRC там нужен SAT solver, поправьте меня, я статью читал уже некоторое время назад.

PS
в том графике, что там написано ИМХО можно сделать только ооочень в общих чертах что-то.

--
Best wishes,
Y

[Maxim Taldykin]

Ага, SAT. Только сначала нужно из кода и пачки аксиом построить то,
что этот SAT будет решать.
Но это я пока не дочитал.

Как я понял genfft сам написан на окамле и по описанию преобразования
генерит сишный код.
Наложением патчика можно заставить его генерить код на хаскеле.
А дальше что? Этот код матчится с аксиомами, делаются эквивалентные
программы и ищутся самые быстрые?

23 ноября 2009 г. 14:23 пользователь Yakov ZAYTSEV <iak...@gmail.com> написал:

[Yakov ZAYTSEV]

genfft написан на окамле
патч делает так, что genfft выводит программу на хаскелл, а именно, абстрактный синтаксис оочень рано, кажется, никакие преобразования еще не выполняются к этому моменту.
понятно, что так я не стал писать разборщик.
потом есть строчка
> main = putStr (show tr)
>  where tr = compileForSharc $ transProg $ <абстрактный синтаксис>
это печатает очередное IR :-)
я работаю над генератором кода для SHARC сейчас.

я не брался прикидывать как вхрячить конвейер вроде denali. я виделил все стадии в отдельные monad transformers из расчета, чтобы было потом удобно менять.

пока у меня ничего нет кроме того что можно найти в textbook material. и еще месяц наверное не будет, у меня есть другие задачи, и пока я этой занимаюсь по остаточному принципу. :-(

я собираюсь по-немногу переписывать то, что есть в Coq.

можно для хакатона придумать что-нибудь отвлеченное, напр., генератоор разборщиков булевых грамматик [1]пописать на haskell. ;-)

[1] http://users.utu.fi/aleokh/boolean/

2009/11/23 Maxim Taldykin <jor...@gmail.com>

--
Best wishes,
Y

[Maxim Taldykin]

Btw, denali во многом смахивает на equality saturation
(http://cseweb.ucsd.edu/~rtate/publications/eqsat/).
E-graph из denali это почти Program Execution Graph из eqsat, только в
последнем ещё и циклы попытались поддержать.
В бэкенде почти тот же самый SAT, для матчинга с аксиомами
используется Rete против congruence closure (не знаю что такое) в
denali.

23 ноября 2009 г. 15:07 пользователь Yakov ZAYTSEV <iak...@gmail.com> написал:

[Yakov ZAYTSEV]

congurence closure есть в Ахульмане упр6.30 (2-е издание)
про это много написано в Term Rewriting and All That (супер-книжка!), которую я еще не дочитал :-)

что такое equation saturation я не понял :-) видимо, что-то из области term rewriting тоже. надо вдумчиво прочитать статью.

про Program Execution Graph я где-то видел.. может в Advanced Compiler Design and Implementation Muchnick'а.. приду домой - гляну.

зато я глянул по диагонали на их следующую работу по извелечению оптимизаций из доказательств:

To implement an optimization in our approach, all the
programmer needs to do is provide a simple concrete example of
what the optimization looks like. Such an optimization instance
consists of some original program and the corresponding transformed
program.

и занес эти статьи в To-Do :-) спасибо!

по поводу второй статьи у меня появилась идея для хакатона.
что если сделать certifying compiler для proof-carrying кода для простых арифметических выражений (с присваиванием)? ;-)
это

• мне кажется по силам для пары дней (по крайней мере чтобы довести до прототипа) для пары человек (ну, так на вскидку)
• позволит попробовать применить подход из второй статьи в проекте.

как думаешь?

кстати, еще

http://www.cis.udel.edu/~cavazos/nips-sl2-final.pdf

для планирования инструкций, после genfft получаются очень длиные basic blocks

PS
я в описании добавил строчку про инициативу в нашей компании

The project is a part of the initiative at our company. Consult http://oorts.ru/main.html for the futher details about this project (in Russian) and other projects

PPS
так а с этим eqsat'ом у тебя уже есть опыт? почему подкинул ссылку?

2009/11/24 Maxim Taldykin <jor...@gmail.com>

--
Best wishes,
Y

[Maxim Taldykin]

Вторую статью (optimizations from proofs) я ещё не видел, судя по
аннотации, штука интересная.

C eqsat'ом опыта нету, хотел уломать начальство попробовать в проекте
(компилятор запросов к бд), но начальство не уломалось, поэтому
немножко поковырял на досуге, но ничего путного не вышло.

Certifying compiler -- отличная идея, пойду почитаю как они делаются.

24 ноября 2009 г. 13:21 пользователь Yakov ZAYTSEV <iak...@gmail.com> написал: