EmbeddedHaskell: Difference between revisions
imported>Rmarko (formatting, ion, haskell embedded blog) |
imported>Rmarko (book links) |
||
(5 intermediate revisions by the same user not shown) | |||
Line 9: | Line 9: | ||
* Haskell embedded blog https://haskellembedded.github.io/ | * Haskell embedded blog https://haskellembedded.github.io/ | ||
* #haskell-embedded on freenode | |||
== Frameworks == | == Frameworks == | ||
Line 20: | Line 21: | ||
* http://ivorylang.org/ | * http://ivorylang.org/ | ||
* http://ivorylang.org/tower-overview.html | * http://ivorylang.org/tower-overview.html | ||
Work in progress book: | |||
* http://48.io/~rmarko/book/ | |||
* Sources https://github.com/HaskellEmbedded/book | |||
==== Repositories ==== | ==== Repositories ==== | ||
Line 43: | Line 49: | ||
===== CAN4DISCO ===== | ===== CAN4DISCO ===== | ||
* https:// | UART2CAN bridge (with kernel support via SLCAN protocol) and CAN development board/firmware. | ||
* https:// | |||
* https://github.com/distrap/can4disco | |||
* https://github.com/distrap/can4disco-hw | |||
===== ODrive experimental firmware ===== | ===== ODrive experimental firmware ===== | ||
* https:// | Brushless DC motor controller firmware for ODrive board. | ||
* https://github.com/distrap/lambdadrive | |||
* https://hackaday.io/project/11583-odrive-high-performance-motor-control/ | * https://hackaday.io/project/11583-odrive-high-performance-motor-control/ | ||
===== HEXAMON Firmware ===== | |||
Beehive monitoring node firmware. | |||
* https://github.com/lucansky/hexamon-firmware | |||
===== Various ===== | |||
* https://github.com/distrap/ivory-tower-base | |||
* https://github.com/distrap/ivory-tower-canopen | |||
* https://github.com/distrap/ivory-tower-hxstream | |||
* https://github.com/distrap/ivory-tower-helloworld | |||
==== Working with Ivory Tower ==== | ==== Working with Ivory Tower ==== | ||
Line 89: | Line 112: | ||
# try talking to /dev/f4uart | # try talking to /dev/f4uart | ||
# bsp-uart-test app accepts ' | # bsp-uart-test app accepts characters '1' for output on and '2' for output off | ||
screen /dev/f4uart 115200 | screen /dev/f4uart 115200 | ||
}} | }} | ||
== Atom == | |||
* https://github.com/tomahawkins/atom | |||
Atom is a Haskell EDSL for designing hard realtime embedded software. | |||
Based on guarded atomic actions (similar to STM), Atom enables highly concurrent | |||
programming without the need for mutex locking. In addition, | |||
Atom performs compile-time task scheduling and generates code with deterministic | |||
execution time and constant memory use, simplifying the process of timing verification | |||
and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, | |||
Atom eliminates the need and overhead of RTOSes for many embedded applications. | |||
== Copilot == | == Copilot == | ||
Line 97: | Line 132: | ||
* https://leepike.github.io/Copilot/ | * https://leepike.github.io/Copilot/ | ||
== | Copilot is a stream (i.e., infinite lists) | ||
domain-specific language (DSL) | |||
in Haskell that compiles into embedded C. | |||
Two compiler backends are available, both of which | |||
generate constant-time and constant-space | |||
C code: | |||
* ''copilot-c99'' targets Atom language | |||
* ''copilot-sbv'' targets SBV language | |||
=== Tutorials === | |||
* https://github.com/leepike/copilot-discussion/blob/master/tutorial/copilot_tutorial.pdf | |||
== Ion == | == Ion == | ||
* https://github.com/HaskellEmbedded/ion | * https://github.com/HaskellEmbedded/ion | ||
* https://haskellembedded.github.io/posts/2016-09-23-introducing-ion.html | |||
Ion is a (heavily experimental) Haskell EDSL for concurrent, realtime, embedded programming. | |||
It performs compile-time scheduling, and produces scheduling code with constant memory usage | |||
and deterministic execution (i.e. no possibility for divergence). | |||
Ion targets Ivory to perform code generation. It generates scheduling code to be called | |||
at regular intervals (e.g. from an interrupt). |
Latest revision as of 08:50, 2 April 2019
"Life is too short to C" -- Adluc
There are now serveral ways to generate C code for embedded applications with domain specific languages embedded in Haskell. This allows us to use type system and powerful compiler to catch errors sooner and get close to 'if it compiles it works' experience for embedded world.
Links
- Haskell embedded blog https://haskellembedded.github.io/
- #haskell-embedded on freenode
Frameworks
Ivory Tower
The Ivory Language is an eDSL for safe systems programming. You can think of Ivory as a safer C, embedded in Haskell.
The Tower Language is an eDSL for composing Ivory programs into real-time systems. Tower programs specify communication channels, tasks, and signal handlers, and generate Ivory code which implements scheduling and communication for real-time operating systems.
Work in progress book:
Repositories
- https://github.com/GaloisInc/ivory/
- https://github.com/GaloisInc/tower/
- https://github.com/GaloisInc/ivory-tower-stm32/
- https://github.com/GaloisInc/smaccmpilot-stm32f4/
- https://github.com/GaloisInc/smaccmpilot-build
- https://github.com/GaloisInc/gidl
Papers
- Guilt Free Ivory https://github.com/GaloisInc/ivory/blob/master/ivory-paper/ivory.pdf
- Building Embedded Systems with Embedded DSLs https://github.com/GaloisInc/smaccmpilot-experiencereport/raw/master/embedded-experience.pdf
Projects
Local projects
CAN4DISCO
UART2CAN bridge (with kernel support via SLCAN protocol) and CAN development board/firmware.
ODrive experimental firmware
Brushless DC motor controller firmware for ODrive board.
- https://github.com/distrap/lambdadrive
- https://hackaday.io/project/11583-odrive-high-performance-motor-control/
HEXAMON Firmware
Beehive monitoring node firmware.
Various
- https://github.com/distrap/ivory-tower-base
- https://github.com/distrap/ivory-tower-canopen
- https://github.com/distrap/ivory-tower-hxstream
- https://github.com/distrap/ivory-tower-helloworld
Working with Ivory Tower
Prepare environment
Install stack first - http://docs.haskellstack.org/en/stable/install_and_upgrade/
<syntaxhighlight lang="bash">mkdir embedded cd embedded git clone https://github.com/GaloisInc/ivory/ git clone https://github.com/GaloisInc/tower/ git clone https://github.com/GaloisInc/ivory-tower-stm32/</syntaxhighlight>
Running UART test
Test application located in
<syntaxhighlight lang="bash">cd ivory-tower-stm32/ivory-bsp-tests</syntaxhighlight>
<syntaxhighlight lang="bash"># set platform to f4 discovery cat > default.conf [args] platform="f4discovery"
make bsp-uart-test cd bsp-uart-test
- now look around carefuly
- oO
- Oo
- ...
- then flash it
arm-none-eabi-gdb --ex 'target extended-remote /dev/f4gdb' \
--ex 'monitor swdp_scan' \ --ex 'attach 1' \ --ex 'load' image'
- try talking to /dev/f4uart
- bsp-uart-test app accepts characters '1' for output on and '2' for output off
screen /dev/f4uart 115200</syntaxhighlight>
Atom
Atom is a Haskell EDSL for designing hard realtime embedded software. Based on guarded atomic actions (similar to STM), Atom enables highly concurrent programming without the need for mutex locking. In addition, Atom performs compile-time task scheduling and generates code with deterministic execution time and constant memory use, simplifying the process of timing verification and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, Atom eliminates the need and overhead of RTOSes for many embedded applications.
Copilot
Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in Haskell that compiles into embedded C. Two compiler backends are available, both of which generate constant-time and constant-space C code:
- copilot-c99 targets Atom language
- copilot-sbv targets SBV language
Tutorials
Ion
- https://github.com/HaskellEmbedded/ion
- https://haskellembedded.github.io/posts/2016-09-23-introducing-ion.html
Ion is a (heavily experimental) Haskell EDSL for concurrent, realtime, embedded programming. It performs compile-time scheduling, and produces scheduling code with constant memory usage and deterministic execution (i.e. no possibility for divergence).
Ion targets Ivory to perform code generation. It generates scheduling code to be called at regular intervals (e.g. from an interrupt).