I'm an embedded developer 2 weeks into learning nim and I'm trying to see if Nim's type system can approach the "Type States" described in in Chap 4 of The Embedded Rust Book (esp section 4.4). Here is my first partial attempt: gist (doesn't compile). I've made an "illformed AST", so I obviously need course correction.
Type States is not something that is easy to read (especially in Rust), but they seem a good (zero-cost abstraction) way to guide the user toward correct use of the API. In this case, we're trying to prevent certain procs from being called when not appropriate for the current state of a fictional GPIO peripheral (i.e. don't call .set_high() when the GPIO is configured as an input).
So it's a broad question and I'm hoping to learn from the discussion as well as connect to other embedded developers.
For my next attempt, I was going to see if an object variant could be employed to solve this.
thanks,
!!Dean
Your gist does not contain enough but I managed to correct the first proc for you:
type
Peripheral* = ref object of RootObj
GPIO* = ref object of Peripheral
GpioConfig*[Tenable, Tdirection, Tmode] = object
periph: GPIO # no need to have fields of generic parameters when the parameters only serve for checking
Disabled = object
Enabled = object
Output = object
Input = object
PulledLow = object
PulledHigh = object
HighZ = object
DontCare = object
proc into_disabled(self: GPIO): GpioConfig[Disabled, DontCare, DontCare] =
GpioConfig[Disabled, DontCare, DontCare](periph: self)
That said, the whole approach seems a bit off for Nim. In Nim you would create a DSL that doesn't let you get away with invalid states.
import std/[options, macros]
type
Direction = enum
Input, Output
GpioConfig[
TEnabled: static bool,
TDirection: static Option[Direction]
] = object
proc initGpioConfig(): GpioConfig[false, none(Direction)] =
discard
proc enable(_: GpioConfig[false, none(Direction)]): GpioConfig[true, none(Direction)] =
discard
proc disable[T](_: GpioConfig[true, T]): GpioConfig[false, none(Direction)] =
discard
proc setDirection(_: GpioConfig[true, none(Direction)], direction: static Direction): GpioConfig[true, some(direction)] =
discard
var config = initGpioConfig()
assert not compiles config.disable()
assert not compiles config.setDirection(Input)
var enabled = config.enable()
var redisabled = enabled.disable()
var input = enabled.setDirection(Input)
assert input is GpioConfig[true, some(Input)]My line of work prohibits metaprogramming.
That's crazy. Like a mathematician who is prohibited from using integrals. ;-)
Yes static data types are not included in the type at runtime. To elaborate further though with huantian's example we can disable the =copy hook to make it so you init a config and only ever have a single owner as follows:
import std/[options, macros]
type
Direction = enum
Input, Output
InternalConfig = object
GpioConfig[
TEnabled: static bool,
TDirection: static Option[Direction]
] = distinct InternalConfig
proc `=copy`[T, Y](config: var GpioConfig[T, Y], src: GpioConfig[T, Y]) {.error.}
proc initGpioConfig(): GpioConfig[false, none(Direction)] =
discard
proc enable(cfg: sink GpioConfig[false, none(Direction)]): GpioConfig[true, none(Direction)] =
result = (typeof result)(cfg)
proc disable[T](cfg: sink GpioConfig[true, T]): GpioConfig[false, none(Direction)] =
result = (typeof result)(cfg)
proc setDirection(cfg: sink GpioConfig[true, none(Direction)], direction: static Direction): GpioConfig[true, some(direction)] =
result = (typeof result)(cfg)
proc main() =
let config = initGpioConfig()
assert not compiles config.disable()
assert not compiles config.setDirection(Input)
let enabled = config.enable()
let redisabled = enabled.disable()
#let a = enabled.setDirection(Input) # Does not compile since `redisabled` now 'owns' the 'config'
let reenabled = redisabled.enable()
let input = reenabled.setDirection(Input)
assert input is GpioConfig[true, some(Input)]
main()
Interesting topic.
If the target is to guide the user toward correct use of an API, can Nim 2.0 effect system help in this direction?
@dwhall
My line of work prohibits metaprogramming
| My line of work prohibits metaprogramming
What does this mean? I work in embedded, too, not like, misra-level or anything but I've never come across any restrictions limiting the level of abstraction. Wouldn't mplab/harmony/all those code configurators from microchip count as metaprogramming?
DO-178 governs how software is written for safety-critical avionics systems and it really puts the guardrails on how one writes code. Metaprogramming is considered a code-translation. It is allowable in certain circumstances, but requires extra scrutiny. We like to avoid extra scrutiny when possible.
In 25 years, I've never written a malloc. Yes, seriously. The last 10 years have been in aviation and I've only written 4 macros using the cpp. The only vendor tools I've used are debuggers and tools that make loadable configuration binaries (not executable code).
I'm not using Nim at work, yet. I'm going to see if I can use it when we make tools that must become a .exe. We avoid "fancy" features even when coding our tools. Keeps us in the zone.
malloc is very different from "meta programming" though, malloc is all about runtime flexibility (allocation of unknown sizes with unknown lifetimes), meta programming is about raising the level of abstraction so that programs become shorter. Not that "meta programming" means much anyway.
But it's a futile discussion, it's not like you can influence the authors of DO-178 and tell them to abandon counter-productive, ill-defined restrictions. Or maybe you can.
I think Zig would be more aligned with that ethos of no-surprises, no code generation. Nim is never going to be that. I came to Nim for embedded because my philosophy is: having code that's written at the right level of abstraction is how to write comprehensible code, and clear, comprehensible, (self-) documented code is the path to correctness.
But that's just a personal theory, and i will never write code that puts people's lives at stake, (insha'Allah)
The DO-178 standard was mainly defined for the C language and I don't think it is strictly applicable for other languages like Nim.
That's true but the bureaucrats will likely simply "adapt" the rules from C to anything else as it's easier than thinking things through.
DO-178 governs how software is written for safety-critical avionics systems and it really puts the guardrails on how one writes code. Metaprogramming is considered a code-translation. It is allowable in certain circumstances, but requires extra scrutiny. We like to avoid extra scrutiny when possible.
Ah make sense. Briefly looking through that spec definitely reminds me of IECEX explosive environment safety standards I've worked on before. Any changes you make need to vetted and run through auditors, etc. I mean they force you to follow processes which is good and all. On the other hand much of it was really up to the auditors and certification companies you use as to the exact processes that are needed / required.
Interestingly, it looks like they consider the compiler codegen part of this "code translation". Well according to this guide: https://www.rapitasystems.com/files/MC-WP-011%20DO-178C%20Verification_2.pdf
Just pondering here. That'd certainly provide interesting challenges for using Nim in that environment. Though in theory Nim's C output could be run through existing C compiler / checkers, perhaps with some tweaks.
I think Nim's effect system could be very useful for ensuring compliance to rules (e.g. no allocations, etc). Perhaps expanded to control factors like IO accesses only occur in certain modules, etc. Especially if faults could be tied to specific tasks/threads in a time bound fashion by calling specific hooks on defects.
How do y'all handle failures, like say integer overflow or a sensor returning erroneous date, or plain old bit flips?
malloc is very different from "meta programming" though, malloc is all about runtime flexibility (allocation of unknown sizes with unknown lifetimes), meta programming is about raising the level of abstraction so that programs become shorter.
Understood. I jumped ahead in my thoughts and was giving an example that not only is programming for embedded systems different than most other kinds of programming, but there are different realms within embedded that have their own quirks.
The DO-178 standard was mainly defined for the C language and I don't think it is strictly applicable for other languages like Nim.
C, Ada and C++ are the three most prevalent languages used in aviation and the DO-178 standard is applied to those and any other who is willing to qualify the compiler. The requirements of DO-178 does make some languages more difficult to comply than others.
Reading that Nim's type system was like Ada's was what really caught my ear.
How do y'all handle failures, like say integer overflow or a sensor returning erroneous date, or plain old bit flips?
Integer overflow is a feature, not a failure <smiley>. Floating point exceptions, now those keep us up at night. Some groups prefer software floating point libraries over hardware floating point units because the software is able to report errors while the hardware does not (or at least you'd have to go check a value after every computation).
Regarding bit flips, the entirety of the hardware and software system is considered. So, level-A (life-critical) stuff is going to have ECC RAM to correct single-bit errors, detect 2 bit errors and a processor interrupt will be triggered in the latter case. A forced reset of the partition (the level-A process) or the entire system is one possible way to handle it. It you can't trust RAM, restart the world.