About Me!

This blog is about my musings and thoughts. I hope you find it useful, at most, and entertaining, at least.

Résumé [PDF]

Other Pages

Quotes

Links

Presence Elsewhere

jim@jimkeener.com

GitHub

BitBucket

Type-madness, Part 1: Enforcing simple constraints with types

Date: 2016-10-18
Tags: programming types c++

I've begun work on APBduino, a basic implementation of Automatic-Permissive Block Signalling system for an Arduino. (I'll have to write more on that.) After a bit of mulling, I realized that a lot of the core logic is (unsurprisingly) similar to Ladder Logic. As such, I am working on another project that will allow a basic form of Instruction List, a standard method of programming the PLCs Ladder Logic runs on. My implementation is called µIL (micro IL, styled uIL).

Since I don't have access to the spec, only some PLC manuals I've found online, and am not aiming for 100% spec compatibility, I decided to use this as a chance to learn more about the C++ type system by implementing two constraints via types: stack-depth protection and setting outputs only once. These two additions will help prevent errors when specifying the ladder logic. The first by preventing illegal operations, the later by disallowing, otherwise valid, but confusing programs.

While implementing these, I had two other main goals as well: stack-only allocation and code size. Not having to dynamically allocate memory at run-time makes static analysis easier and also removes a few classes of errors.

Something else I kept in mind while writing all of this was that it'll be running a teensy-weensy microprocessor. I need the code to be space efficient. Luckily, much of the type magic doesn't map to executable code, allowing very complex things to be done in the compiler, on my relatively giant, humongous, speed-daemon of a laptop.

The first allows us to define certain amounts of memory to be defined at compile-time, and any operation that would violate those memory constraints will cause a compile-time error. Since accessing invalid or an unbounded amount of memory would be pernicious to the system, not allowing these operations to compile eliminates a large class of errors.

The last is more interesting. Ladder logic was originally implemented as Relay logic, and the entire "program" (electrical circuit) executed simultaneously. Multiple outputs to the same relay could cause unexpected results. Now that Ladder logic is implemented in a microprocessor, the programs are executed in serial. However, they become easier to reason about if every output is set once. Similar to a computer program that changes a variables value all of the time, it can make jumping into a program to understand it difficult. Since hardware is being controlled, and often safety-critical systems are being implemented, easily reasoning about the software is extremely useful.

To tease the read, as this will be discussed in the next post, the single-setting of an output was a tour through some of the more interesting type mangling and compile-time expressions. The basic idea here is that each operation returns the set of outputs (actually their types) that have already been set, e.g. OR will return the same set, SET will return the old set unioned with the type being set. Now that magic that makes this happen: using enable_if and some helper types and compile-type expressions to disallow that list to have repeated types. (I must admit, while I thought of doing this, my actual implementation was based on some help and examples from ##C++ (webchat).) All of these checks also happen at compile-time and also generate no code. Needing to have each output be its own type isn't a terrible solution, and should be a near zero-cost abstraction since the type need only extend another type, not implement any code.

One potential issue that I'm still exploring is each templated class will generate code for each unique set of template parameters. This isn't ideal. What I decided to do was create another class that does the actual implementation of all of the methods, but isn't templated; it takes the type parameters as argument as needed. This allows for the templated class to be inlined and for no code to be generated for it, only the functions calls to the class implementing the logic. I'm testing if -Os is good enough to know that, or if I need to forcibly tell the compiler to inline it. We'll discuss in a later post.

Stack Protection

A stack is a type of data-structure where objects are placed on the top each time they're added, and removed from the top when they're removed (think a stack of paper on a desk); this is known as Last-In First-Out (LIFO) or First-In Last-Out (FILO). (Compare to a queue, like a British queue, an American "line", waiting for an event where the first person in the line is the first person in: First-In First Out (FIFO).)

Stacks, among other things, are used by computers to keep track of nested computations. Nested computations? Imagine we have:

python (2+2) * (3 + 3)

We need to compute 2+2 and 3+3 before we can compute their product. In order to do so, we need to temporarily store the value of one of the additions, while we compute the other. One means of doing this is to use a stack. (Another way would be one of the additions in another memory address or register while the next addition is performed.) Some machines, called Stack Machines, have no registers or memory in the extreme case, there are various levels of "hybrid" machines with registers and direct memory access. Many Virtual Machines, like the JVM, Cython, YARV, Forth, as well as some classic architectures are implemented like this as it makes the implementation simpler and easier to validate. Let's compute 3+3 and push it on the stack:

``` Stack


6
```

Let's "push" it onto the stack

Now, let's compute 2+2 and push it onto the stack:

``` Stack


6 4 ```

We can then "pop" both 4 and 6, add them, and push the result onto the stack.

``` Stack


10 ```

(This is very similar to how Reverse Polish Notation is written and implemented.)

Why is this important for us? IL has stack and most instructions affect the current location in the stack, the rest control which location in the stack is being examined.

Since there is a finite amount of memory, the depth of the stack is intrinsicly limited. If we would like to enforce that limit -- or a more restrictive one, say only 4 deep instead of all of memory -- at compile time, we need to be able to know both the current stack location, and the maximum number of slots in the stack. One way of using this information is to have each instruction return the slot in the stack that the next instruction will affect.

Stack protection was relatively straight-forward to implement using the C++ templating system. The basic idea is based around embedding the maximum and current stack depths into the type of the current IL mnemonic. We can do this because any constant expression and type can be used as a template parameter in C++, not just types; in this case, we're using an integer as our template parameter.

By initializing the first instruction as depth 0 and with a pre-allocated stack (i.e. of a known size, which gets transmuted into the max stack depth), each following instruction returns the appropriate stack depth, e.g.

  • AND returns the same
  • PUSH returns a location one larger than the current
  • ORP returns one fewer (and ORs the current and one fewer's values, storing the result in the one fewer than current location.

We will always know the current and maximum depths at compile time. The maximum depth is a value that is passed from mnemonic to mnemonic unchanged, and is set when the initial space for the stack is allocated, which we must do at compile time (no dynamic allocation!). We also know the current stack depth because each mnemonic returns the location the next one is to use. For most mnemonic this is the same value as the one it operated on. For PUSH and ORP it is one higher or lower, relatively, than the current one. Inductively we can show that this value is always known. For example:

LOAD true (@0 max 4) -> true - - - @0 max 4) AND false (@0 max 4) -> false - - - (@0 max 4) PUSH (@0 max 4) -> false - - - (@1 max 4) LOAD true (@1 max 4) -> false true - - (@1 max 4) ORP (@1 max 4) -> true - - - (@0 max 4)

Because these are all constant expressions, at compile time we can check to ensure that the operation will return a stack depth less than the max depth and greater than or equal to zero. Since these checks happen at compile time, no code is generated to perform these comparisons. The fast code is that which doesn't exist. The following is a sample implementation.

~~~~{.language-cpp pre_class="line-numbers"}

include

/ * Used by pos to verify a value is greater than or equal to zero. */ template struct positive { const static bool value = -1 < VAL; }; / * Used by enable_if to verify a value is greater than or equal to zero. */ template using pos = typename std::enable_if::value>::type;

/ * Used by lt to verify that the first param is less than the second. */ template struct less_than { const static bool value = VAL < MAXVAL; }; / * Used by enable_if to verify that the first param is less than the second. */ template using lt = typename std::enable_if::value>::type;

/ * LadderRun represents a sequence of instructions to execute each cycle. * * OK, so this isn't the best name for this; it's more like a single * instruction. * * The STACK_DEPTH paramter represents the current depth of the stack, * i.e. the index into the stack array. * * The MAX_STACK_DEPTH parameter represents the size of the array * representing the stack, stored in the reference stack. * */ template< int8_t STACK_DEPTH, int8_t MAX_STACK_DEPTH> class LadderRung { private: bool (&stack)[MAX_STACK_DEPTH]; public: / * Constructs a new object with a reference to a stack. * * Reference to ensure we don't copy the stack by value, and hence * have multiple copies of it. */ LadderRung(bool (&base_stack)[MAX_STACK_DEPTH]);

/**
 * Loads a value into the current accumulator (position in the stack).
 */
LadderRung<STACK_DEPTH, MAX_STACK_DEPTH> LOAD(bool val);

/**
 * Logical AND with the paramter and the accumulator (position
 * in the stack).
 */
LadderRung<STACK_DEPTH, MAX_STACK_DEPTH> AND(bool val);

/**
 * Increments the stack depth.
 *
 * The `lt` is required to be valid when the class is created, so the
 * protection comes from the `return` statement generating a class
 * with a new `LadderRung` that is an invalid stack depth.
 */
template<lt<STACK_DEPTH, MAX_STACK_DEPTH>* = nullptr>
LadderRung<STACK_DEPTH+1, MAX_STACK_DEPTH> PUSH();

/**
 * `OR`s the current position and one lower storing in the lower;
 * Decrements the stack depth.
 *
 * The `pos` is required to be valid when the class is created, so the
 * protection comes from the `return` statement generating a class
 * with a new `LadderRung` that is an invalid stack depth.
 */
template<pos<STACK_DEPTH>* = nullptr>
LadderRung<STACK_DEPTH-1, MAX_STACK_DEPTH> ORP();

};

template< int8_t STACK_DEPTH, int8_t MAX_STACK_DEPTH> LadderRung :: LadderRung(bool (&base_stack)[MAX_STACK_DEPTH]) : stack(base_stack) {}

template< int8_t STACK_DEPTH, int8_t MAX_STACK_DEPTH> LadderRung LadderRung :: LOAD(bool value) { stack[STACK_DEPTH] = value; return LadderRung(stack); }

template< int8_t STACK_DEPTH, int8_t MAX_STACK_DEPTH> LadderRung LadderRung :: AND(bool value) { stack[STACK_DEPTH] = stack[STACK_DEPTH] & value; return LadderRung(stack); }

template template*> LadderRung LadderRung :: PUSH() { return LadderRung(stack); }

template template*> LadderRung LadderRung :: ORP() { stack[STACK_DEPTH - 1] = stack[STACK_DEPTH - 1] | stack[STACK_DEPTH]; return LadderRung(stack); }

void print_stack(bool (&stack)[4]) { std::cout << "Stack: " << stack[0] << "," << stack[1] << "," << stack[2] << "," << stack[3] << std::endl; } int main() { std::cout << "Test running" << std::endl;

bool stack[] = {false, false, false, false}; LadderRung<0,4>(stack) .LOAD(false) .AND(true); print_stack(stack);

bool stack2[] = {false, false, false, false}; LadderRung<0,4>(stack2) .LOAD(true) .AND(true); print_stack(stack2);

bool stack3[] = {false, false, false, false}; LadderRung<0,4>(stack3) .LOAD(false) .AND(true) .PUSH() .LOAD(true) .AND(true) .ORP(); print_stack(stack3);

/ * Max Stack Depth exceeded bool stack4[] = {false, false, false, false}; LadderRung<0,4>(stack4) .PUSH() .PUSH() .PUSH() .PUSH() .PUSH(); print_stack(stack4); /

/ * Stack Underflow bool stack4[] = {false, false, false, false}; LadderRung<0,4>(stack4) .ORP(); print_stack(stack4); / return 0; } ~~~~

Better errors

As a side note, the above was done to encapsulate the checks in the type system, not just at compile-time. However, using a static_assert in PUSH and ORP can produce better error messages and occur where someone jumping into the code would expect it to occur, i.e. in the function, not in creating the return value.

~~~language-cpp pre_class='line-numbers" data-start="75' /* * Increments the stack depth. * * The lt is required to be valid when the class is created, so the * protection comes from the return statement generating a class * with a new LadderRung that is an invalid stack depth. / LadderRung PUSH();

/**
 * `OR`s the current position and one lower storing in the lower;
 * Decrements the stack depth.
 *
 * The `pos` is required to be valid when the class is created, so the
 * protection comes from the `return` statement generating a class
 * with a new `LadderRung` that is an invalid stack depth.
 */
LadderRung<STACK_DEPTH-1, MAX_STACK_DEPTH> ORP();

~~~

~~~language-cpp pre_class='line-numbers" data-start="124' template template*> LadderRung LadderRung :: PUSH() { static_assert(STACK_DEPTH + 1 < MAX_STACK_DEPTH, "Max Stack Depth exceeded"); return LadderRung(stack); }

template LadderRung LadderRung :: ORP() { static_assert(STACK_DEPTH > 0, "Min Stack Depth exceeded"); stack[STACK_DEPTH - 1] = stack[STACK_DEPTH - 1] | stack[STACK_DEPTH]; return LadderRung(stack); } ~~~

The static_assert are checked at compile-time, as would the type-based check above, but, as mentioned, are a bit more friendly to the programmer. However, the mechanism of passing the current and maximum depth around still needs to be in place.

Tune in next time

In the next installment, we'll investigate using a similar technique to help ensure we don't set an output multiple times in the same program