Microlog - A Datalog for Microcontrollers and other Interactive Systems

Current Progress, Semantics, Code Examples for Declarative Programming in Interactive Systems

Jump to: Introduction Publications and Related Work Language and Semantics Static Analysis Runtime and Compilation pyMicrolog (Python DSL)

Authors: Mario Wenzel, Stefan Brass

Introduction

Logic and declarative programming is often and successfully used as parts of desktop and server applications. We value the declarative techniques because it is easier to write programs that relate closely to the specification (or even write compilable specifications) and show their correctness. Declarative programming has found its place in most computer science curricula in some form (often Haskell and Prolog) as well. But especially in logic programming the applications often are theoretical or only used as part of a larger system. The parts that interact with the outside world are usually written in an imperative fashion. For embedded systems, where rule-based interaction with the outside world is often the majority of the application, declarative programming is an avenue not well explored.

Microlog is a specific dialect of Datalog closely related to the Dedalus language that includes IO operations. Our declarative language Microlog is a language that allows us to model both program state and side effects in a declarative manner. Based on Datalog, Microlog has strong foundations in relational algebra and logic. As we do not allow ad-hoc queries or a dynamic extensional database, we can split our logic program into disjoint parts; the parts that provably use finite memory over time are compiled into finite state machines while the residual program is evaluated with a naive algorithm that is optimized to use as little memory as possible. Our goal is to declaratively program microcontrollers and give static safety guarantees for data-driven interactive programs on microcontrollers

Publications and Related Work

Our Publications

Related Work

Language and Semantics

microlog is a variant of Datalog. Every predicate has an additional implicit argument that represents time.
A normal datalog rule (deductive rule) p(a1,a2,..) :- q(a1,a2,..). actually means a deduction in the current timestamp: p(T,a1,a2,..) :- q(T,a1,a2,..).
Inductive rules p(a1,a2,..)@next :- q(a1,a2,..). actually means a deduction in the next timestamp: p(S,a1,a2,..) :- q(T,a1,a2,..), successor(T,S).
In inductive rules, we addionally allow a call to an external source of computation. In addition, it is allowed to write quantifier-free atomic formulas in a chosen theory in the rule body, which are queried as Boolean oracles.

Static Analysis (Memory Restriction and Safety Guarantees)

We have different approaches of giving static guarantees about microlog programs. Our current focus are safety guarantees.

Example (heating control)

We can easily describe a system where the heating not only shuts off in a room with an open window (a common use case for home automation), but also in all (other) rooms connected via open doors (see Figure 2). The function calls are from a fictitious library that wraps communication to the sensors and actors, #open is a C constant from that library. It is usually the case that control to hardware is provided by some library, as protocols like I2C need to be observed or read analog voltage levels need to be translated to values in expected units. The static rules of hasWindow and adjacent are the configuration of our program to our specific example home with two connected rooms where the second room has window. A user, if this program was provided to them, would only need to add those facts to configure it for their home.
You can see the full example in the down below under heating/lopstr.dl

The initial state in this example is state 0. The variables (memory locations) for the return values are called slots. In this example we need two slots. One for the return value of each sensor (one door, one window).
The transition function is normalized to disjunctive normal form.

The transition code is executed in the loop-function provided by the runtime. This allows to run multiple FSMs and normal deduction steps in lockstep. In the Arduino runtime the infinite loop is implicit, in the LEGO EV3 runtime it is explicit.

byte _fsm1_state = 0;
int _fsm1_slot__1;
int _fsm1_slot__2;

void loop()
{
if (_fsm1_state == 0) {
  { int Doorstate = doorstate(1, 2); _fsm1_slot__1 = Doorstate;}
  { int State = windowRead(2); _fsm1_slot__2 = State;}
  {if (!(_fsm1_slot__2 == open)) {_fsm1_state = 0} else
   if ((_fsm1_slot__1 == open) && (_fsm1_slot__2 == open)) {_fsm1_state = 1} else
   if ((_fsm1_slot__2 == open) && !(_fsm1_slot__1 == open)) {_fsm1_state = 2} else ;}
  } else
if (_fsm1_state == 1) {
  { heating_off(1);  }
  { heating_off(2);  }
  { int Doorstate = doorstate(1, 2); _fsm1_slot__1 = Doorstate;}
  { int State = windowRead(2); _fsm1_slot__2 = State;}
  {if (!(_fsm1_slot__2 == open)) {_fsm1_state = 0} else
   if ((_fsm1_slot__1 == open) && (_fsm1_slot__2 == open)) {_fsm1_state = 1} else
   if ((_fsm1_slot__2 == open) && !(_fsm1_slot__1 == open)) {_fsm1_state = 2} else ;}
  } else
if (_fsm1_state == 2) {
  { heating_off(2);  }
  { int Doorstate = doorstate(1, 2); _fsm1_slot__1 = Doorstate;}
  { int State = windowRead(2); _fsm1_slot__2 = State;}
  {if (!(_fsm1_slot__2 == open)) {_fsm1_state = 0} else
   if ((_fsm1_slot__1 == open) && (_fsm1_slot__2 == open)) {_fsm1_state = 1} else
   if ((_fsm1_slot__2 == open) && !(_fsm1_slot__1 == open)) {_fsm1_state = 2} else ;}
  } else;
}

Runtime and Compilation

Our current compiler is written in Haskell and translates Microlog programs to C with a runtime that executes the rules in every state. Partial programs that can be represented as finite state machines are compiled that way.

Example programs with an Arduino and Lego EV3 runtime. Some programs show specific optimizations or transformations (toy), while others show specific application. The example programs have last been compiled {{microlog.update}}.

A protoype compiler is available here.
Download the example compilation data here.

Further Examples

Please wait while the example sources are loading...
Choose Program:
Choose Setting:
Choose Template

pyMicrolog

pyMicrolog is a DSL for Python (3.6+) using the Microlog semantics. The main differences to Microlog are due to Python's dynamic nature: all relations are variadic, oracles and io-calls are done via function reference instead of formula/function name.

Here you can see the declaration, rules, and tiny imperative surrounding program of a two-player version of the popular connect-4 game. You can play the game in the terminal here. Below you'll find the source code extract.

The full sources for pyMicrolog can be found on github.


from pymicrolog import relation, START, NEXT, call, Program, variable, variables

# shared global state
board = {}

# relations
setup = relation("setup")
winner = relation("winner")
phase = relation("phase")
player = relation("player")
current_player = relation("current_player")
column = relation("column")
row = relation("row")
top_of = relation("top_of")
besides = relation("besides")
dropped = relation("dropped")
marker = relation("marker")
new_marker = relation("new_marker")

# interactions
set_board = call(lambda C, R, P: board.update({(C,R):P}))
ask_column = call((lambda P: int(input("Player {}: Which column to drop in? ".format(P)))))
announce = call(print)

# some variables we use
C, R, P = variables(*"CRP")
C1, C2, C3, C4 = variables("C1", "C2", "C3", "C4")
R1, R2, R3, R4 = variables("R1", "R2", "R3", "R4")
P2 = variable("R2")

rules = [
setup()@START,

phase("print")@NEXT <= setup(),
phase("ask")@NEXT <= phase("print") & ~winner(...),
phase("gather")@NEXT <= phase("ask") & ~winner(...),
phase("print")@NEXT <= phase("gather") & ~winner(...),
phase("halt")@NEXT <= winner(...),

player(1),
player(2),
current_player(1)@START,

] +
[column(x) for x in range(7)] +
[row(x) for x in range(6)] +
[top_of(X+1,X) for X in range(5)] +
[besides(X+1,X) for X in range(6)] + [

marker(C, R, 0) <= setup() & row(R) & column(C),
new_marker(C, 0, P) <= dropped(P, C) & marker(C, 0, 0),
new_marker(C, R, P) <= dropped(P, C) & ~marker(C, 0, 0) & marker(C, R, 0) & top_of(R, R2) & ~marker(C, R2, 0),
marker(C, R, P)@NEXT <= marker(C, R, P) & ~new_marker(C, R, ...),
marker(C, R, P)@NEXT <= new_marker(C, R, P),
set_board(C, R, P)@NEXT <= marker(C, R, P) & ~new_marker(C, R, ...),
set_board(C, R, P)@NEXT <= new_marker(C, R, P),

ask_column(P)@NEXT <= phase("ask") & current_player(P),
dropped(P, C) <= current_player(P) & player(P) & ask_column(P, C) & column(C) & marker(C, ..., 0),

current_player(P2)@NEXT <= dropped(...,...) & player(P2) & ~current_player(P2),
current_player(P)@NEXT <= ~dropped(...,...) & current_player(P),

winner(P) <= player(P) & marker(C1, R, P) & besides(C1, C2) & besides(C2, C3) & besides(C3, C4) & marker(C2, R, P) & marker(C3, R, P) & marker(C4, R, P),
winner(P) <= player(P) & marker(C, R1, P) & top_of(R1, R2) & top_of(R2, R3) & top_of(R3, R4) & marker(C, R2, P) & marker(C, R3, P) & marker(C, R4, P),
winner(P) <= player(P) & marker(C1, R1, P)  & top_of(R1, R2) & top_of(R2, R3) & top_of(R3, R4) & besides(C1, C2) & besides(C2, C3) & besides(C3, C4) & marker(C2, R2, P) & marker(C3, R3, P) & marker(C4, R4, P),
winner(P) <= player(P) & marker(C1, R1, P)  & top_of(R1, R2) & top_of(R2, R3) & top_of(R3, R4) & besides(C2, C1) & besides(C3, C2) & besides(C4, C3) & marker(C2, R2, P) & marker(C3, R3, P) & marker(C4, R4, P),
announce("Player", P, "has won")@NEXT <= winner(P),
]

# the imperative part of printing the board
for s in Program(rules).run_generator(extended_state=True):
  if (phase, ("halt",)) in s:
    break
  if (phase, ("print",)) in s:
    print("=======")
    print("0123456")
    print("-------")

    for Y in range(5, -1, -1):
        for X in range(7):
            print(board[(X, Y)], end="")
        print("")
    print("")