Anatomy of A Periodic Program

The program body is here,

http://disi.unitn.it/~abeni/RTOS/periodic-1.c

First to mention that a periodic program is that it is activated periodically, i.e. the program wakes up periodically (it is ready for execution). Under Linux kernel, you could trace such wake up events (sched_wake_up) through ftrace. The sample program uses a real-time timer ITIMER_REAL to create periodic interrupts. The timer is set initially 2000000 us (=2s) and thence 5000us (5ms).

start_periodic_timer(2000000, 5000);

In further detail, that is

signal(SIGALRM, sighand);

Notice that sighand is the name of the call-back function. Whenever there a SIGALRM fires within the program, the function sighand is called. Though in the example it is a do-nothing function. The signal function registers sighand as the call-back, but it doesn't execute it.

The following does the job to set periods and the first round offset (this is to ensure the periodicity since we are still initializing the timer before the real periodic part comes). The timer ITIMER_REAL fires the signal SIGALRM when the timer count decreases to zero (expires), as a consequence, signal goes executed.

setitimer(ITIMER_REAL, &t, NULL);

So there are periodic interrupts on which a futile function is run (whence the program wakes up). The following infinite loop does sleeping till the signal is fired (pause()), then an in-genuine job_body() is under way. The job body function is "controlled" within 5ms such that all interrupt signals are captured on-time.

    while(1) {
        wait_next_activation();
        job_body();
    }

Conclusion

An implementation of periodic programs follows this pattern,

void *PeriodicTask(void *arg)
{
    <initialization>;
    <start periodic timer, period = T>;
    while (cond) {
        <read sensors>;
        <update outputs>;
        <update state variables>;
        <wait next activation>;
    }
}

Region Automata and Zone Automata

As a sequel of a previous article on timed automaton (link), here we introduce its computational models.

1. Region

Why region automata? Timed automata have infinite state space (time be divided into infinite pieces), region automata give a finite partition of timed automata such that the computation becomes possible.

Intuition A region is a set of equivalent states. The partition divides the state space into different equivalent classes (regions).

Temporal constraint given by this grammar $\phi := x > c | x < c | x = c | \phi \wedge \phi$, $c$ must be an integer constant (to ensure non-zenoness)

Equivalent class The set of states which satisfies the same set of temporal constraints.

Region equivalence states are equivalent due to being in the same region, they are either within the integer grid, on the $x=c$ or $y=c$ axes, or above/below the diagonal of the integer grid. (see Figure 1.)

Fig 1. Regions as equivalent classes

Remind that largest constant relevant $c$ is actually the ceiling of $x_i$, i.e. $c = \lceil x_i \rceil$. Figure 2 is an example of partitions (regions) of the state space of a timed automaton. Not only are those shadowed areas regions, but also segments of lines (they usually are a result of clock resetting).

Fig 2. Regions on a 2-clock timed automaton

A further example Figure 3 shows the region representation of a simple timed automaton. Location $F$ is shadowed since it may loop forever, a bad design (livelock).

Fig 3. Timed automaton represented in regions

Time-abstract bisimulation If $w \simeq v$, $w,v \in l$, 1) after action $a$, $w'$ is in the region of location $l'$, so is $v'$; 2) $\forall d \exists d' . w+d \simeq v+d'$. They are respectively the transition on action and the transition on delay.

Region equivalence relation is a time-abstract bisimulation ($\simeq$).

Region reset The clock for all equivalent states is reset, hence the operation projects the whole region onto the clock axis (i.e. a line of shadow).

2. Zone

Why zone automata? Regions are still too many, we can force them collapse into unions of regions, where the unions are convex, i.e. no angles are larger than 180 degrees.

Zone Zones are so-called symbolic state (conjunction of regions). Formally, $Z = (s, \varphi)$, that is to start from a location (state) $s$ in a timed automaton, we make a conjunction of regions specified by temporal constraint $\varphi$.

Zone automaton A transition system for zones. Formally, $Z = (Q, Q^0, \Sigma, R)$, set of zones, initial zone, set of transition labels, transition relation.

Symbolic transition It may involve operations such as intersection (conjuncts), delay (stretches diagonally as x,y propagate in time simultaneously), reset (projects a shadow on the time axis). For a zone $Z = (s, \varphi)$, the transition is denoted as $\mathsf{succ}(\varphi, e)$, where $e$ is the label of switch. When $e$ is executed, $Z$ propagates by time till the time constraint $\varphi$ is met. The action is thus invoked. Proceed with a reset if it is needed.

Fig 4. Transitions on Zone Automaton

Figure 4 showed a symbolic transition from location n to m, i.e. $(n, 1 \leqslant x \leqslant 4, 1 \leqslant y \leqslant 3) \rightarrow (m, x>3,y=0)$

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012, link

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please refer the link in the references.

A Glimpse of Timed Automata

Terms

Timed Automaton Intuitively, an automaton with clocks, the transitions from state to state are constrained by time. Formally, $A = (L, L^0, \Sigma, X, I, E)$, respectively the set of locations (states), the set of initial locations, labels, clocks, invariants, the set of edges (transitions) $$E = \{ (s, a, \varphi, \lambda, s') | s,s' \in L, a \in \Sigma, \varphi \text{:clock constraints}, \lambda \subseteq X \}$$

Clock a stopwatch in this context, i.e. clocks are to measure the elapsed time, it can be reset.

Guard Boolean comparison between the clock and some integer value, serves as a constraint for the switch from one location to another

Action the label of transition, used to synchronize actions among several timed automata

Reset set the clock to time 0 and meanwhile the clock starts ticking again

Invariant a time constraint residing inside the state which must be respected when staying within such state, otherwise, it must move out.

Deadlock cases are, there are no more allowed moves (due to bad design of automata).

Example

We quote an automaton from this slide ^[1],

Figure 1. An Example Timed Automaton

• $s_i$'s are state labels
• two clocks present $x$, $y$
• after action $a$, it can only stay in $s_1$ for no more than $1$ time unit
• action $d$ can occur only when clock $y$ reads more than $2$ (due to the guard $y>2$)

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012

Life of Me

So it comes to this moment that I shall write what a true blogger practices. Not those lifeless pieces of knowledge, not wild copies of diffused computer techniques, or minute excerpts or backup discoveries. After all, after hunting after the ocean of webpages to obtain a very portion of nutrition, one wonders about the behind scenes and how the world bloggers think. Simply, a real person to talk with, on the somewhat crossed paths, or even colleagues of the same kind. You know, the laws of attraction.

The prime purpose of this blog was nothing but put aside some tricks that I came across so that later on I can easily find them. So why this turn? Why didn't I write these lines from the very beginning?

Well, I tried, in my second mother tongue. I was a pride self-assumed writer. I have jotted down many of my own guts, most of them obscure and in an archaic style so that no one except those who know me well could bother reading. My journalist-to-be brother definitely attempted to seek a way to understand me, being elder made him fraternal and faster-matured. We had a geographic segregation since every of us had departed to different universities, his in northwest and mine northeast. The span was the width of China. My mother tongue is a Long dialect. And I quickly mastered Mandarin with the spicy of northeastern accent while I stayed four years in the college. I admit that I have quite a talent of mimicking sounds, but not so much on memory. I was terrified to force myself to remember at grade two. We were asked to recite a short paragraph, only three lines. I had fought so hard but I could not manage. Nonetheless, I grew up, with a rather noteworthy fame at the place. During my university period, I observed and struggled, sought and sighed, alone. We met a few times, each time ended up arguing until both were tired. There was a lack of perception. We are seemingly divided by fate. It lasted until today and I have moved to Europe while he becomes a real news reporter. We haven't talked in depth, only some family greetings. There have not been acknowledgeable comments of my writings. My perplexed groaning was like a grain dropped into a pond. Until one day I was provoked to take off everything from my first blog. The blog host set one post as hidden. I thus wrote a python snippet to scrape out my fruits. My major is Informatics, not to brag. To write a piece of running code you need aches as the same when I construe the very picture in my head and put them into readable words. They do take time more than you could plan. I am still on this steep rising learning curve. I had a plea to terminate the amateur author life. Being in a prestigious European university and studying science you could just accord that writing is too much a luxurious leisure. The reality smashed in my face saying nothing is necessary but survival. Music is just in the background to sooth you in hardship. Parties belong to the drinking dudes. News is all of a manipulation of public thought. Religion, a salvation when you have lost your secular hope and become desperate. Talent for languages in such a multilingual context, a not-so-relevant skill to have for decoding the mystery of mathematics, to mention, Computability and Computational Complexity etc. To speak of truth, right now I am into this far-reaching nearby leisure again. Then why?

To solve this, I need to tell more of my latest deviation from the thesis work. I have taken my liberty to taste the whole of Yann's Life of Pi, so the Ang Lee's film. Shall we put this page down at our feet, and scream we are back?! We will see. I had meant to write a comment of Pi, but what do you see?

Abstraction in Model Checking

Finite Transition System $M = (S, I, R, L)$, respectively the set of states, the set of initial states, the set of transition relations, labels. Simply put, a computational model, similar to Finite State Machine.

Which Computation? Well, model checking. $M \models \varphi$

Why abstraction? Too many states to compute and the abstraction reduces the number of states.

Why abstraction works? The existential-quantified properties (ECTL) are preserved after the abstraction ($M$ simulates $M'$, i.e., $M$ has whatever $M'$ has), that is, $M' \models \varphi \rightarrow M \models \varphi$. (But not vice versa!)

Now let's go to terms.

Abstraction function $h: S \rightarrow S'$

Simulation $M$ simulates $M'$ when each transition of $M'$ has a corresponding one in $M$. The simulation is the set of pairs of states $p \subseteq \{ (s,s') | s \in S, s' \in S' \}$ that records such behavior. It is the set denotation of the abstract function $h$.

Bisimulation The simulation applies on both sides. According to property preservation, $M \models \varphi \rightarrow M' \models \varphi$. As a consequence, $M \not \models \varphi \rightarrow M' \not \models \varphi$, otherwise we reach a contradiction.

$M$ simulates $M'$, plainly put, $M$ is an abstraction (simulation) from $M'$.

What about universal-quantified properties? (in LTL or ACTL) They are preserved when $M'$ simulates $M$. That is, $$M' \models \varphi \rightarrow M \models \varphi$$ Yes, same conclusion but different condition. Still, the reverse doesn't hold.

Exercise

Credit: ~rseba, disi.unitn.it

If we draw a relation $p = \{(S_{ij}, T_i) | \text{for all possible } i,j \}$, we see (with effort) that $p$ is a simulation from $M$ to $M'$ (i.e. $M'$ simulates $M$). Verify it by the rigorous definition, if $(S_{11}, T_1) \in p$, $(S_{11}, S_{12}) \in R_M$, $\exists (T_1, T_1) \in R_{M'}$ s.t. $(S_{12}, T_1) \in p$. So are the rest transition relations of $M$. Hence, the universal-quantified property preservation applies. e.g. if $\varphi$ is pure boolean, $$M' \models \mathbf{AG} \varphi \rightarrow M \models \mathbf{AG} \varphi$$

To note that the reverse doesn't hold. For instance, $(S_{13}, T_1) \in p$, $(T_1, T_1) \in R_{M'}$, $\forall j. \nexists (S_{13},S_{1j}) \in R_{M}$ s.t. $(S_{1j},T_1) \in p$.

Shell: Copy to Clipboard

With the help of xclip, one can copy the whole text file to the system clipboard

$ sudo apt-get install xclip

The following copys the content of foo file to clipboard (X selection)

$ cat foo | xclip -selection c

Once copied, put it into a file

xclip -o > foo

A Walk-through of A Character Device Driver

This article explains how to compile a sample Linux character device driver and how to read and write from the device.

A Sample Character Device Driver

The sample code is a copy of ldd3's example code sleepy.

/*
 * sleepy.c -- the writers awake the readers
 *
 * Copyright (C) 2001 Alessandro Rubini and Jonathan Corbet
 * Copyright (C) 2001 O'Reilly & Associates
 *
 * The source code in this file can be freely used, adapted,
 * and redistributed in source or binary form, so long as an
 * acknowledgment appears in derived source files.  The citation
 * should list that the code comes from the book "Linux Device
 * Drivers" by Alessandro Rubini and Jonathan Corbet, published
 * by O'Reilly & Associates.   No warranty is attached;
 * we cannot take responsibility for errors or fitness for use.
 *
 * $Id: sleepy.c,v 1.7 2004/09/26 07:02:43 gregkh Exp $
 */

#include <linux/module.h>
#include <linux/init.h>

#include <linux/sched.h>  /* current and everything */
#include <linux/kernel.h> /* printk() */
#include <linux/fs.h>     /* everything... */
#include <linux/types.h>  /* size_t */
#include <linux/wait.h>

MODULE_LICENSE("Dual BSD/GPL");

static int sleepy_major = 0;

static DECLARE_WAIT_QUEUE_HEAD(wq);
static int flag = 0;

ssize_t sleepy_read (struct file *filp, char __user *buf, size_t count, loff_t *pos)
{
 printk(KERN_DEBUG "process %i (%s) going to sleep\n",
   current->pid, current->comm);
 wait_event_interruptible(wq, flag != 0);
 flag = 0;
 printk(KERN_DEBUG "awoken %i (%s)\n", current->pid, current->comm);
 return 0; /* EOF */
}

ssize_t sleepy_write (struct file *filp, const char __user *buf, size_t count,
  loff_t *pos)
{
 printk(KERN_DEBUG "process %i (%s) awakening the readers...\n",
   current->pid, current->comm);
 flag = 1;
 wake_up_interruptible(&wq);
 return count; /* succeed, to avoid retrial */
}


struct file_operations sleepy_fops = {
 .owner = THIS_MODULE,
 .read =  sleepy_read,
 .write = sleepy_write,
};


int sleepy_init(void)
{
 int result;

 /*
  * Register your major, and accept a dynamic number
  */
 result = register_chrdev(sleepy_major, "sleepy", &sleepy_fops);
 if (result < 0)
  return result;
 if (sleepy_major == 0)
  sleepy_major = result; /* dynamic */
 return 0;
}

void sleepy_cleanup(void)
{
 unregister_chrdev(sleepy_major, "sleepy");
}

module_init(sleepy_init);
module_exit(sleepy_cleanup);

Makefile

obj-m = sleepy.o
KVERSION = $(shell uname -r)
PWD = $(shell pwd)
all:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) modules
clean:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) clean

Compile The Driver

The ultimate way is to compile it along with a built kernel tree. However, for the time being, installing Linux kernel headers would suffice. It should already be installed by default.

sudo apt-get install linux-headers-$(uname -r)

If installed, type

make

Load and Remove The Driver

You will see some new files are generated, including sleepy.ko, to load this module

sudo insmod sleepy.ko

To unload,

sudo rmmod sleepy

Read from and write to the device

The sleepy is created with a dynamic major, we need to create a device file for it. First get the major number,

$ cat /proc/devices | grep sleepy
250 sleepy

Then create a node under /dev, c is to create a character file, 0 is its minor number.

sudo mknod /dev/sleepy c 250 0

Now we can read and write the device using C library function read, write, or from shell

echo "sleep" > /dev/sleepy
cat /dev/sleepy

Though what sleepy does is that it makes the reader process fall asleep while the writer process wakes all readers up.

#include <fcntl.h>
#include <unistd.h>

int fd;
char buffer[32];

fd = open("/dev/sleepy", O_RDONLY);
read(fd,buffer,10);