/[dtapublic]/pubs/papers/20060327_phd_topic_proposal/phdtopicpropa.tex
ViewVC logotype

Annotation of /pubs/papers/20060327_phd_topic_proposal/phdtopicpropa.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 8 - (hide annotations) (download) (as text)
Fri Oct 7 03:14:27 2016 UTC (6 years, 2 months ago) by dashley
File MIME type: application/x-tex
File size: 43536 byte(s)
Commit of Ph.D. topic proposal.
1 dashley 8 %$Header: /home/dashley/cvsrep/e3ft_gpl01/e3ft_gpl01/dtaipubs/cron/2006/phdtopicpropa/phdtopicpropa.tex,v 1.20 2006/03/27 00:10:30 dashley Exp $
2     \documentclass[letterpaper,10pt,titlepage]{article}
3     %
4     %\pagestyle{headings}
5     %
6     \usepackage{amsmath}
7     \usepackage{amsfonts}
8     \usepackage{amssymb}
9     \usepackage[ansinew]{inputenc}
10     \usepackage[OT1]{fontenc}
11     \usepackage{graphicx}
12     %
13     \begin{document}
14     %-----------------------------------------------------------------------------------
15     \title{Ph.D. Topic Proposal}
16     \author{\vspace{2cm}\\David T. Ashley\\\texttt{dta@e3ft.com}\\\vspace{2cm}}
17     \date{\vspace*{8mm}\small{Version Control $ $Revision: 1.20 $ $ \\
18     Version Control $ $Date: 2006/03/27 00:10:30 $ $ (UTC) \\
19     $ $RCSfile: phdtopicpropa.tex,v $ $ \\
20     \LaTeX{} Compilation Date: \today{}}}
21     \maketitle
22    
23     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
24     %
25     \begin{abstract}
26     This document describes my Ph.D. research interests and provides
27     supporting information. The interests
28     (described in \S{}\ref{srin0}) revolve around the mathematical
29     basis of timed automata systems and code generation
30     from timed automata models.
31     \end{abstract}
32    
33     \clearpage{}
34     \pagenumbering{roman} %No page number on table of contents.
35     \tableofcontents{}
36     \clearpage{}
37     \listoffigures
38     \clearpage{}
39    
40     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
41     %Force the page number to 1. We don't want to number the table of contents
42     %page.
43     %
44     \setcounter{page}{1}
45     \pagenumbering{arabic}
46     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47    
48     \section{The Timed Automata Framework}
49     \label{staf0}
50    
51     The framework of timed automata isn't commonplace in electrical
52     engineering, so this section provides
53     a description.
54    
55    
56     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
57    
58     \subsection{The Framework}
59     \label{staf0:stfw0}
60    
61     The formal framework of timed automata consists of systems of
62     automatons, each with discrete states, transitions, and
63     timers that can be reset to zero on transitions.
64    
65     The framework includes synchronization mechanisms between automatons (i.e.
66     automatons may interact in well-defined ways)\@. Synchronization mechanisms
67     consist of ``soft'' synchronization mechanisms and ``hard'' synchronization
68     mechanisms.
69    
70     \begin{itemize}
71     \item \emph{Soft} synchronization mechanisms involve one automaton having transition
72     functions that involve the discrete state or timers of another automaton.
73     \item \emph{Hard} synchronization mechanisms involve events. The semantics
74     of an event require two or more
75     automatons to make corresponding transitions at exactly the same time.
76     \end{itemize}
77    
78     The details of the framework aren't especially important,
79     and there are several
80     variations on the framework\footnote{Variations include
81     substates, differences in the semantics of events, and dynamics that go beyond
82     $\dot{t} = 1$ (i.e. hybrid systems).} that don't change the essential properties.
83    
84     The essential properties of the framework (that don't change with the variations) are:
85    
86     \begin{itemize}
87     \item A system of timed automata that interact via synchronization
88     mechanisms can be mathematically combined into a single
89     larger automaton with a single
90     discrete state space.
91     \item There is some symbolic method of reasoning about what values
92     timers can attain in each discrete state (polytopes, DBMs, etc.).
93     \item The symbolic reasoning about timer values often allows reasoning about
94     properties of the system (reachability, liveness, etc.).
95     \end{itemize}
96    
97     Timed automata are recognizeable to any embedded software engineer as
98     ``state machines''. A typical automotive embedded system consists of many
99     features and software components involving discrete state. For example,
100     software to control an automobile drivetrain with features like automatic 4-wheel drive
101     as well as sensor and actuator failure modes tends to have a very large discrete
102     space.
103    
104     As a contrived example of a system of timed automata, consider the problem of
105     controlling a drawbridge with one motor and two limit switches so that it goes up and down
106     with period $K_D + K_U$ (Fig. \ref{fig:staf0:stfw0:000}).
107    
108     \begin{figure}
109     \centering
110     \includegraphics[width=4.0in]{system01.eps}
111     \caption{Example Timed Automata System (Drawbridge Control)}
112     \label{fig:staf0:stfw0:000}
113     \end{figure}
114    
115     Assume that when raising the drawbridge, it is adequate to energize the motor
116     until the limit switch $U$ closes. However, when closing the drawbridge,
117     it is necessary to energize the motor for time $K_L$ beyond
118     when the limit switch $D$ closes (the $B_{DOWNLOCK}$ state in
119     Fig. \ref{fig:staf0:stfw0:01}).
120    
121     One way to design such a system is with two automata
122     (Fig. \ref{fig:staf0:stfw0:00} and Fig. \ref{fig:staf0:stfw0:01}) interacting via
123     synchronization mechnisms.
124    
125     The automaton of Fig. \ref{fig:staf0:stfw0:00} alternates between two
126     states with period $K_D + K_U$. At any point in time, the state of this
127     automaton indicates whether the drawbridge should be down or up.
128    
129     \begin{figure}
130     \centering
131     \includegraphics[height=2.5in]{exta01.eps}
132     \caption{Example Timed Automaton (Drawbridge Target Position Determination)}
133     \label{fig:staf0:stfw0:00}
134     \end{figure}
135    
136     The automaton of Fig. \ref{fig:staf0:stfw0:01} directly
137     determines the energization of the bridge motor as a function of
138     the limit switches $D$ and $U$, the discrete state of the automaton
139     of Fig. \ref{fig:staf0:stfw0:00}, and time.
140     In the $B_{IDLE}$ state, the motor is deenergized.
141     In the $B_{UP}$ state, the motor is energized to move the
142     drawbridge up. In the $B_{DOWN}$ and $B_{DOWNLOCK}$ states,
143     the motor is energized to move the drawbridge down.
144    
145     \begin{figure}
146     \centering
147     \includegraphics[width=4.6in]{exta02.eps}
148     \caption{Example Timed Automaton (Drawbridge Motor Control)}
149     \label{fig:staf0:stfw0:01}
150     \end{figure}
151    
152     Mathematically, the automata of Figs.
153     \ref{fig:staf0:stfw0:00}
154     and
155     \ref{fig:staf0:stfw0:01} can be combined to give the automaton of
156     Fig. \ref{fig:staf0:stfw0:02}\@. This mathematical operation is sometimes called the
157     ``shuffle'' operation.
158    
159     \begin{figure}
160     \centering
161     \includegraphics[width=4.6in]{exta03.eps}
162     \caption{Example Timed Automaton (Shuffle of Fig. \ref{fig:staf0:stfw0:00} and Fig. \ref{fig:staf0:stfw0:01})}
163     \label{fig:staf0:stfw0:02}
164     \end{figure}
165    
166     In Fig. \ref{fig:staf0:stfw0:02}, each of the eight discrete states
167     corresponds to one discrete state from Fig. \ref{fig:staf0:stfw0:00}
168     and one discrete state from In Fig. \ref{fig:staf0:stfw0:01}.
169     The initial state $A_{D}B_{IDLE}$ corresponds to the initial state
170     from In Fig. \ref{fig:staf0:stfw0:00} paired with the initial state
171     from Fig. \ref{fig:staf0:stfw0:01}.
172    
173     The noteworthy features of Fig. \ref{fig:staf0:stfw0:02} are:
174    
175     \begin{itemize}
176     \item It is the result of a mathematical algorithm applied to
177     Figs. \ref{fig:staf0:stfw0:00} and \ref{fig:staf0:stfw0:01}.
178     If the underlying system consisted of more than two automata, the
179     algorithm could be applied repeatedly to generate a single automaton with
180     a single large discrete state space.
181     \item The upper bound on the number of discrete states in the shuffle
182     of two automata is the product of the number of discrete states
183     in each. Note, however, that $A_{D}B_{UP}$ and $A_{U}B_{DOWN}$
184     don't ``truly'' exist. The reason is that the synchronization
185     mechanisms between the two automata ensure that these states
186     are instantly exited as soon as they are entered. Thus, a system
187     of equivalent functionality can be constructed with six discrete
188     states rather than eight.
189     \end{itemize}
190    
191     Although the preceding example is contrived, it illustrates the flavor
192     of the framework and how separate automata with synchronization mechanisms can be
193     combined (and perhaps also ``separated'' or ``factored'', \S{}\ref{srin0:star0}).
194    
195     It should also be apparent that tools can verify a great deal about
196     the system through symbolic manipulation. Properties that can be verified
197     include:
198    
199     \begin{itemize}
200     \item \emph{Reachability:} it can be symbolically determined whether
201     or not each state is reachable (the algorithms involve determining
202     symbolically which values timers can achieve in each discrete state and
203     comparing that information against transition functions---some transitions
204     cannot ever be taken).
205     \item \emph{Liveness:} it can be symbolically determined whether the system
206     can enter a state where no inputs to the system can cause all of a
207     set of states to be reachable.
208     \end{itemize}
209    
210     The example comes \emph{very} close to the way practical
211     software systems are constructed. Generally, state machines in
212     software have transition functions that involve time and the states of
213     other state machines.
214    
215    
216     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
217    
218     \subsection{Human Tendencies}
219     \label{staf0:shtd0}
220    
221     My experience in industry is that human beings do badly with the
222     design of stateful controllers. Typical tendencies:
223    
224     \begin{itemize}
225     \item \textbf{Bloating of the controller state space:}
226     \;It is very common for engineers to design a controller with
227     a discrete state space that is too large. The prototypical
228     example is an engineer who finds a way to implement a purely combinational
229     function using sequential logic.
230    
231     In the most humorous case (purely combinational logic implemented as
232     sequential logic),
233     the system usually behaves correctly. Serious software defects
234     most typically come about through \emph{subtle} design mistakes. A typical software defect
235     involves two or more software components with some interaction that enter
236     states such that the software can't recover.
237     \item \textbf{Inability to comprehend all possible behaviors of the system:}
238     Very stateful systems tend to be incompatible with human cognitive
239     ability. Even when the problem is well-defined and when the controller and
240     plant are operating perfectly, human beings don't do
241     well at considering every possible behavior.
242     \item \textbf{Inability to comprehend how the system may behave in the presence
243     of failures:}
244     Very stateful systems are often designed to be tolerant of certain types
245     of sensor and actuator failures (usually in the sense that the failures will
246     be detected and the system will employ a different algorithm to operate without
247     a specific sensor or actuator)\@. Such fault detection and tolerance
248     normally complicates the software design substantially.
249    
250     However, even without designed-in fault tolerance, there is the need to
251     design controllers to tolerate the faults that can occur in any practical system.
252     Specific scenarios that must be tolerated:
253    
254     \begin{itemize}
255     \item Spurious reset of the controller (which will normally reset the controller
256     to its initial state but leave the plant undisturbed). (This directly implies that
257     the system must recover from the initial state of the controller combined with
258     any state of the plant.)
259     \item State upset of the controller (due to electrical noise, internal software errors,
260     etc.). (This directly implies that the system must recover from any state of
261     the controller combined with any state of the plant.)
262     \end{itemize}
263    
264     Except in simple cases, human beings don't have the cognitive capacity to consider
265     all possible behaviors when both the controller and the plant may start in any state.
266     \end{itemize}
267    
268     One example that comes to mind from product development is an automobile transfer case controller
269     where it was discovered that if the electrical connector was removed, the transfer case mechanical
270     components repositioned, and the electrical connection restored; the controller would not
271     recover into normal operation. Human beings are not good at mentally exploring all possibilities, and even
272     a disciplined manual process can't be used because the combinations sometimes number in the thousands
273     or more. A mathematical framework and tool support are required.
274    
275    
276     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
277    
278     \subsection{Code Generation}
279     \label{staf0:scgn0}
280    
281     In most engineering environments, software is generated
282     from software designs that involve timed automata. (Some of the techniques
283     used to create compact code are described in \S{}\ref{sfrr0}.)
284    
285     For some types of systems, there has been success in using
286     existing tools to generate code directly from the software design
287     (using tool chains from \emph{The Math Works} or \emph{I-Logix}). It is,
288     however, known from experience that a clever human programmer can generate
289     more compact code than any existing tool; so code generation tools have
290     not penetrated cost-sensitive automotive products involving 32K of FLASH or less.
291    
292     There are two primary arguments against manual generation of code:
293    
294     \begin{itemize}
295     \item Code is redundant with respect to a software design.
296     In general, it does not make economic sense to maintain redundant
297     information using human labor.
298     \item The act of optimizing implementations typically destroys the
299     clear relationship between design and code. Furthermore, changes
300     to the design---sometimes even small ones---can invalidate the
301     mathematical basis for certain optimizations. Optimized code becomes
302     unmaintainable. It would be more economical to evaluate the viability
303     of optimizations and to generate code using software tools (rather than
304     human labor).
305     \end{itemize}
306    
307    
308     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
309    
310     \subsection{Formal Verification of Properties}
311     \label{staf0:svpr0}
312    
313     Typical design tools provide simulation capability, and there is a large
314     body of theory and best practice about how to design test cases based on
315     a stateful design.
316    
317     Still, the following problems remain:
318    
319     \begin{itemize}
320     \item Systems with a large discrete state space elude human
321     understanding.
322     \item It is very laborious to test systems with a large discrete
323     state space.
324     \item It isn't possible to fully test systems with a large
325     discrete state space.
326     \item It is possible (and common) to make a good faith effort at
327     comprehensively testing systems but still to overlook
328     unacceptable behavior.
329     \end{itemize}
330    
331     \emph{Simulation and testing are not enough.} For complex safety-critical
332     systems, simulation and testing do not provide enough assurance about the
333     behavior of the system.
334    
335     Formal verification of properties would involve making mathematical assertions
336     about how the system must and must not behave, and then allowing
337     tools to verify the properties.
338    
339     Possible types of properties:
340    
341     \begin{itemize}
342     \item \emph{Required behavior:}
343     For example: \emph{When the brake pedal switch is closed,
344     the brake lights must always come on within 200ms.}
345     \item \emph{Required absence of behavior:}
346     For example: \emph{The airbags can never deploy without at least one
347     body deformation sensor indicating body deformation.}
348     \item \emph{Liveness:}
349     For example: \emph{A certain set of states is always reachable by manipulating certain
350     inputs.}
351     \end{itemize}
352    
353     The only tool I'm aware of that allows formal verification of properties
354     is UPPAAL. However, the modeling framework of
355     UPPAAL isn't rich enough to support practical embedded systems.\footnote{The
356     tool chains from \emph{The Math Works} and \emph{I-Logix} don't attempt
357     formal verification at all.}
358    
359     I would tend to view formal verification of properties as a last line of defense
360     against egregious software defects (i.e. as a practice that cannot stand alone)\@.
361     Formal verification should be combined with all other known
362     best practices.
363    
364    
365     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
366    
367     \section{FLASH/ROM Reduction Techniques}
368     \label{sfrr0}
369    
370     In this section, I mention some of the FLASH/ROM reduction techniques
371     used by human programmers. Important points:
372    
373     \begin{itemize}
374     \item All of the techniques have a mathematical basis.
375     \item The techniques are complex to apply and best carried out by tools.
376     \item The mathematical basis of the techniques is non-trivial. There are
377     many unexplored corners.
378     \item The techniques distort the correspondence (i.e. the resemblance)
379     between design and code, and make code unmaintainable (it would be
380     better only to generate code from designs and never to maintain
381     code directly).
382     \end{itemize}
383    
384     The list of techniques presented is not exhaustive (far more techniques
385     exist).
386    
387     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
388    
389     \subsection{General Paradigm of Software Construction for Small Microcontrollers}
390     \label{sfrr0:sgsc0}
391    
392     This discussion is confined entirely to systems where a stateful design is
393     implemented directly as code (with no tabulation or compression of the design).
394     Other paradigms are possible. For example, at least one tool on the market implements
395     stateful designs as state transition tables that are evaluated at runtime by
396     a table interpreter. My experience with these types of systems is that there
397     is always a real-time performance penalty (but certainly not always a
398     FLASH penalty). My research interests do also include event-driven systems
399     and systems where the design is not implemented directly as code; but these
400     systems are not mentioned for brevity.
401    
402     The most common paradigm for small systems is ``\emph{a collection of cooperating
403     timed automatons}''. The most typical abstraction of these systems is a data-flow
404     diagram, with RAM variables (i.e. global variables) used as the interfaces.
405    
406     There is a body of theory and best practice about what separates good software designs
407     and implementations from bad (Parnas and the classic coupling and cohesion spectrums
408     come to mind). However, in small systems, it simply isn't possible to
409     implement the systems using classic ``good'' programming practice---formal parameters,
410     pointer dereferencing, and access to variables in stack frames all bloat
411     FLASH size under the weak instruction sets typical of small microcontrollers.
412    
413     It is helpful to take a step back and consider the possibility that global variables
414     (the second-strongest form of coupling in the classic coupling spectrum) aren't
415     inherently harmful; but rather that it is the way in which global variables are
416     typically used that causes harm. The harmful aspects of global variables
417     seem to be:
418    
419     \begin{itemize}
420     \item If global variables are tested \emph{and assigned} in more than place,
421     the variable actually becomes an automaton and adds to the
422     state space of the system.
423     \item Global variables lead to unrestrained connectivity: \emph{any}
424     software component can access the variables. Additionally,
425     state is not ``shed'' as functions return (as happens with formal
426     parameters and local variables)\@. This leads to connectivity
427     that often skips levels of the calling tree (making it very
428     difficult to understand the software).
429     \end{itemize}
430    
431     Small systems often have design rules to mitigate the harmful aspects of
432     global variables. The design rules tend to involve these restrictions:
433    
434     \begin{itemize}
435     \item A global variable used as an interface can be assigned by only one
436     software component (a 1-writer, $n$-reader restriction).
437     \item A global variable used as an interface has its readers/writers
438     represented in design documentation (so that the connectivity
439     created by the global variable isn't accidental or unrestrained).
440     \end{itemize}
441    
442     The design rules typically also include provisions for global variables
443     used as interfaces that are tested and assigned by more than one software
444     component (i.e. interface automatons). The simplest example of such an
445     interface is a semaphore that is
446     set \emph{T} by one software component and tested and set \emph{F} by
447     another software component, but the design rules are far more general.
448    
449     Note that tools can be used to allow a system to be phrased in a way
450     consistent with the traditional coupling spectrum but implemented
451     efficiently for small microcontrollers. For example, some compilers
452     are able to analyze the calling tree and place variables of storage
453     class \emph{automatic} into statically overlaid\footnote{Statically overlaid
454     based on the calling tree: one function's automatic variables can be overlaid
455     with another only if an analysis of the calling tree determines that
456     the two functions cannot be active at the same time.} areas of memory rather than
457     in a stack frame. Similar tool support could be developed for the notion of
458     \emph{automatic} bitfields and to restrain the connectivity introduced
459     by global variables to be consistent with the product design.
460    
461    
462     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
463    
464     \subsection{Near versus Far (Addressing Modes)}
465     \label{sfrr0:snvf0}
466    
467     Most small microcontrollers (TMS370C8, 68HC05, etc.) have two
468     non-indexed addressing modes, typically called \emph{direct} and
469     \emph{extended}. Instructions using the direct addressing mode typically
470     have the address encoded as a single byte, and can address only locations
471     \$00 through \$FF\@. Instructions using the extended addressing mode
472     typically have the address encoded as two bytes, and can address
473     locations \$0000 through \$FFFF.
474    
475     For lack of better nomenclature, I'll call the RAM locations that can be addressed
476     using short instructions \emph{near} RAM, and the RAM locations that require
477     long instructions \emph{far} RAM.
478    
479     When fixed RAM locations are used as interfaces (\S{}\ref{sfrr0:sgsc0}),
480     one can save substantial FLASH by allocating the variables that are
481     referenced most often throughout the software into near RAM.
482    
483     In automotive software, variables such as gearshift position and vehicle speed
484     are typically referenced many times throughout FLASH. Most programmers
485     would automatically place these into near RAM.
486    
487     However, for most variables, it isn't obvious whether these should be placed
488     into near or far RAM.
489    
490     Software developers often write small utility programs to scan all software
491     modules to determine the number of references to each variable. This information
492     is then used to allocate the variables with the most references into near RAM.
493    
494     The FLASH savings from using this technique is typically large. As an example,
495     assume there are ten variables each referenced 50 times throughout the software.
496     The savings of placing these variables into near RAM versus far RAM is
497     typically about $50 \times 10 = 500$ bytes of FLASH (more than 1\% of a
498     32K FLASH).
499    
500    
501     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
502    
503     \subsection{Treatment of Time}
504     \label{sfrr0:stot0}
505    
506     The way that time is measured is usually the single most important decision
507     in a small embedded system. Typically, many software components have to
508     measure time intervals, so a suboptimal decision about the mechanisms
509     greatly increases FLASH consumption.
510    
511     The best mechanism known is to arrange all software timers into
512     binary decades and to decrement the timers en masse
513     (Fig. \ref{fig:sfrr0:stot0:00}).
514    
515     \begin{figure}
516     \begin{small}
517     \begin{verbatim}
518     unsigned char modulo_counter;
519     unsigned char timers_modulo_1[MOD1_COUNT];
520     unsigned char timers_modulo_2[MOD2_COUNT];
521     unsigned char timers_modulo_4[MOD4_COUNT];
522    
523     void decrement_timers(void)
524     {
525     int i;
526    
527     modulo_counter++;
528    
529     for (i=0; i<sizeof(timers_modulo_1)/sizeof(timers_modulo_1[0]); i++)
530     {
531     if (timers_modulo_1[i])
532     timers_modulo_1[i]--;
533     }
534    
535     if (modulo_counter & 0x01)
536     {
537     for (i=0; i<sizeof(timers_modulo_2)/sizeof(timers_modulo_2[0]); i++)
538     {
539     if (timers_modulo_2[i])
540     timers_modulo_2[i]--;
541     }
542     }
543    
544     if (modulo_counter & 0x02)
545     {
546     for (i=0; i<sizeof(timers_modulo_4)/sizeof(timers_modulo_4[0]); i++)
547     {
548     if (timers_modulo_4[i])
549     timers_modulo_4[i]--;
550     }
551     }
552     }
553     \end{verbatim}
554     \end{small}
555     \caption{Software Timers Decremented En Masse}
556     \label{fig:sfrr0:stot0:00}
557     \end{figure}
558    
559     When software components must measure time, a byte
560     (\texttt{timers\_modulo\_4[2]}, for example) is set to a non-zero value.
561     A separate software component, usually resembling Fig. \ref{fig:sfrr0:stot0:00} but often
562     implemented in assembly-language,
563     decrements the byte, but not below zero.
564     A test against zero will determine if the time period has expired.
565    
566     The single-byte mechanism combined with binary decades allows any time period
567     to be measured within 1:128. For example, assume that the binary decades are
568     $2^q \times 1ms$ (1ms, 2ms, 4ms, etc.) and then that
569     we wish to measure a time period of 30 minutes. Then
570    
571     \begin{equation}
572     255 (2^q) \geq 1,800,000
573     \end{equation}
574    
575     \begin{equation}
576     q = \left\lceil \log_2 \frac{1,800,000}{255} \right\rceil = 13
577     \end{equation}
578    
579     A timer resolution of $2^{13} = 8,192$ms with a count of 219 or 220 would in practice be used.
580     For most automotive applications, measuring 30 minutes within 8 seconds is acceptable.
581    
582     It is noteworthy that using coarse software timers introduces nondeterminism
583     into the system (although I've never seen a problem in practice) and probably requires
584     some adjustment to timed automata algorithms used for verification of properties.
585    
586    
587     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
588    
589     \subsection{Bitfields of Size One}
590     \label{sfrr0:sbfi0}
591    
592     Many small microcontrollers possess extremely efficient instructions
593     for clearing, setting, and testing individual bits of RAM (especially near
594     bits). It isn't uncommon for a microcontroller to have an instruction that
595     will test a bit and conditionally branch.
596    
597     Note that economies apply only to bitfields of size one. Bitfields of
598     other sizes require the compiler to mask and shift to obtain the value of the
599     bitfield, then to shift and mask to store the value back.
600    
601     The economy of bitfields of size one has several implications for the construction
602     of embedded software.
603    
604     \begin{itemize}
605     \item Variables that are conceptually Boolean should never be
606     maintained as full bytes. Bitfields are more efficient, both
607     in FLASH and RAM.
608     \item In many cases, it is most efficient to maintain discrete state as
609     bitfields rather than as a byte. A state machine with three
610     discrete states is often most effectively implemented as two
611     bitfields with state assignments 0/0, 0/1, and 1/X.
612     \item It is often most effective to evaluate common Boolean subexpressions and store
613     the results in bitfields (\S{}\ref{sfrr0:scse0}).
614     \end{itemize}
615    
616    
617     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
618    
619     \subsection{Equivalence Classing of Discrete States}
620     \label{sfrr0:secd0}
621    
622     The most obvious way to construct a state machine in software is shown in
623     Fig. \ref{fig:sfrr0:secd0:00}. Discrete state is maintained
624     as a byte, and each state has a value $\in \{0, \ldots{}, 255\}$.
625    
626     \begin{figure}
627     \begin{small}
628     \begin{verbatim}
629     switch (state)
630     {
631     default:
632     case 0:
633     {
634     if (some_transition_condition)
635     {
636     state = 1;
637     }
638     break;
639     }
640     case 1:
641     {
642     if (some_other_transition_condition)
643     {
644     state = 0;
645     }
646     break;
647     }
648     case 2:
649     {
650     ...
651     break;
652     }
653     }
654     \end{verbatim}
655     \end{small}
656     \caption{Most Obvious Construction of State Machine in Software}
657     \label{fig:sfrr0:secd0:00}
658     \end{figure}
659    
660     The shortcoming of the approach shown in Fig. \ref{fig:sfrr0:secd0:00} is that
661     state machines are often accompanied by:
662    
663     \begin{itemize}
664     \item Combinational logic that implements combinational functions involving
665     the discrete state of the state machine being considered.
666     \item Transition functions in other state machines that depend on the discrete
667     state of the state machine being considered.
668     \end{itemize}
669    
670    
671     \begin{figure}
672     \begin{small}
673     \begin{verbatim}
674     if (
675     (state == 0) || (state == 13) || (state == 18) || (state == 30)
676     || (state == 31) || (state == 51) || (state == 99)
677     )
678     \end{verbatim}
679     \end{small}
680     \caption{Typical Test for Membership in a Set of Discrete States}
681     \label{fig:sfrr0:secd0:01}
682     \end{figure}
683    
684     This can often lead to tests of the form shown in
685     Fig. \ref{fig:sfrr0:secd0:01}.
686     Such tests are very expensive, both in FLASH consumption and in execution time.
687     A typical compiler must generate many compare instructions.
688    
689     One can make the observation that there are many machine instructions that
690     create equivalence classes within $\mathbb{Z}^+$:
691    
692     \begin{itemize}
693     \item An \emph{AND \#1} instruction may create equivalence classes such as
694     \{0, 2, 4, \ldots{}\} versus \{1, 3, 5, \ldots{}\}. Other \emph{AND} instructions
695     can create more complex equivalence classes.
696     \item A \emph{CMP \#n} instruction usually creates three equivalence classes: the integers less than $n$,
697     $n$, and the integers greater than $n$.
698     \item There are other machine instructions that create different equivalence classes.
699     \end{itemize}
700    
701     The critical question is whether one can assign discrete state values so as to
702     make the best utilization of the equivalence classes that machine instructions
703     naturally create. For example, if a test for 10 distinct discrete states occurs
704     many places in the software, it would make sense to try to assign these
705     state values so that they are part of an equivalence class that can be
706     identified immediately by one or two machine instructions.
707    
708     It should be obvious that if many different tests of discrete state are involved,
709     identifying an optimal or near-optimal assignment of discrete state values and
710     the accompanying tests would be very difficult to do by hand. This type of
711     optimization is best done by software tools.
712    
713    
714     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
715    
716     \subsection{Ordering of Transition Functions}
717     \label{sfrr0:sotf0}
718    
719     It often happens that transition functions have common subexpressions.
720     For example, consider the code snippet in Fig. \ref{fig:sfrr0:sotf0:00}.
721     The subexpression ``\texttt{A \&\& B}'' is common to both transitions
722     out of State 0.
723    
724     \begin{figure}
725     \begin{small}
726     \begin{verbatim}
727     switch (state)
728     {
729     default:
730     case 0:
731     {
732     if (A && B && C)
733     {
734     state = 1;
735     }
736     else if (A && B && !D)
737     {
738     state = 2;
739     }
740     break;
741     }
742     case 1:
743     {
744     ...
745     break;
746     }
747     case 2:
748     {
749     ...
750     break;
751     }
752     }
753     \end{verbatim}
754     \end{small}
755     \caption{State Machine Before Control Flow Removal of Common Subexpression}
756     \label{fig:sfrr0:sotf0:00}
757     \end{figure}
758    
759     The code can be optimized to evaluate this subexpression only once
760     (Fig. \ref{fig:sfrr0:sotf0:01}).
761    
762     \begin{figure}
763     \begin{small}
764     \begin{verbatim}
765     switch (state)
766     {
767     default:
768     case 0:
769     {
770     if (A && B)
771     {
772     if (C)
773     {
774     state = 1;
775     }
776     else if (!D)
777     {
778     state = 2;
779     }
780     }
781     break;
782     }
783     case 1:
784     {
785     ...
786     break;
787     }
788     case 2:
789     {
790     ...
791     break;
792     }
793     }
794     \end{verbatim}
795     \end{small}
796     \caption{State Machine After Control Flow Removal of Common Subexpression}
797     \label{fig:sfrr0:sotf0:01}
798     \end{figure}
799    
800     In the trivial case presented, it is easy to identify the subexpression
801     and rearrange the code so that it is evaluated only once. However, more complex cases
802     involve logical implication; i.e. there is not an identifiable subexpression, but there
803     is still a way to rearrange the code for better efficiency. Such analysis is
804     best done by software tools.
805    
806    
807     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
808    
809     \subsection{Common Subexpression Elimination}
810     \label{sfrr0:scse0}
811    
812     It often occurs that the same subexpression appears in transition functions from
813     more than one discrete state. It can be economical to rearrange the
814     code to evaluate such subexpressions
815     only once. Two approaches occur in practice:
816    
817     \begin{itemize}
818     \item The subexpression is evaluated once, regardless of discrete state, and the
819     result is placed in a temporary variable (often a bitfield if the expression
820     has a Boolean result).
821     \item The evaluation of the subexpression is implemented as a subroutine, and
822     the subroutine is called from more than one transition function.
823     \end{itemize}
824    
825     Each of these two approaches has advantages and disadvantages.
826    
827     Identifying common subexpressions and deciding how to eliminate the FLASH
828     penalty associated with duplicated code is a tedious task and best done
829     by software tools.
830    
831     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
832    
833     \subsection{Farey Series Approximations}
834     \label{sfrr0:sfsa0}
835    
836     Many modern microcontrollers have an efficient integer multiplication
837     instruction, and some also have an efficient integer division instruction.
838     Fixed-point arithmetic is the norm in small microcontroller work, and it
839     is common to want to approximate functions of the form
840    
841     \begin{equation}
842     y = r_I x
843     \end{equation}
844    
845     \noindent{}with $r_I \in \mathbb{R}^+$ and $x,y \in \mathbb{Z}^+$. $r_I$ is the
846     ``ideal'' scaling factor, which may be irrational.
847    
848     If the processor has an integer multiplication instruction but no division
849     instruction, it is usually most effective to choose
850    
851     \begin{equation}
852     r_A = \frac{h}{2^q} \approx r_I,
853     \end{equation}
854    
855     \noindent{}with the division by a power of two implemented via a right shift.
856    
857     However, if the processor also has an integer division instruction, we may choose
858    
859     \begin{equation}
860     r_A = \frac{h}{k} \approx r_I,
861     \end{equation}
862    
863     \noindent{}with $k$ not required to be a power of two. The specific function
864     implemented is usually
865    
866     \begin{equation}
867     y = \left\lfloor \frac{hx}{k} \right\rfloor ,
868     \end{equation}
869    
870     \noindent{}or perhaps
871    
872     \begin{equation}
873     y = \left\lfloor \frac{hx + z}{k} \right\rfloor ,
874     \end{equation}
875    
876     \noindent{}where $z \in \mathbb{Z}$ is used to shift the result so as to
877     provide a tighter bound on the error introduced due to truncation of the
878     division.
879    
880     $h$ and $k$ are constrained by the sizes of operands accepted by the
881     machine instructions ($h \leq h_{MAX}$ and $k \leq k_{MAX}$).
882     There is an algorithm from number theory (involving Farey series and
883     continued fractions) that will allow the selection of $h$ and $k$ subject
884     to the constraints. The algorithm is $O(\log N)$ and so can be applied
885     to find best rational approximations even for processors that accommodate
886     32- or 64-bit operands.\footnote{The computational complexity of the algorithm is
887     a significant point, as $2^{64}$ (or $2^{128}$) is a very large number.}
888    
889     For example, the best rational approximation to $\pi$ with
890     numerator and denominator not exceeding $2^{16}-1$ is 65,298/20,785\@.
891     On a processor with a 16-bit $\times$ 16-bit multiplication instruction and a
892     32-bit / 16-bit division instruction, one can approximate
893    
894     \begin{equation}
895     y = \pi x
896     \end{equation}
897    
898     \noindent{}with
899    
900     \begin{equation}
901     y = \left\lfloor \frac{65,\!298 x}{20,\!785} \right\rfloor
902     \end{equation}
903    
904     \noindent{}very efficiently (typically 2-4 machine instructions).
905    
906    
907     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
908    
909     \subsection{Vertical Counters}
910     \label{sfrr0:svcn0}
911    
912     The traditional arrangement for sequential logic is a
913     \texttt{switch()} statement (this might also be called
914     a ``horizontal'' counter). However, in some applications that must
915     implement many identical sequential mappings, it is
916     efficient to arrange the state vector so that the state of each sequential
917     mapping consists of a bit in the same position from several bytes. This
918     is called a ``vertical'' counter.\footnote{It is suspected that the nomenclature
919     \emph{vertical counter} comes about because if one arranges the 0s and 1s of
920     bytes horizontally, the state of an individual sequential machine consists
921     of a vertical row of bits.}
922    
923     An example of a vertical counter application is 3/3 debouncing---a filtering
924     function where a discrete input must be in the same state for 3 consecutive
925     instants of discrete time before the output may change to that state.
926    
927     If $A$ is the most recent sample, $B$ is the next-most-recent sample,
928     $C$ is the oldest sample, and $O$ is the output (assumed maintained
929     as a RAM location) Fig. \ref{fig:sfrr0:svcn0:00}
930     supplies the Karnaugh map for 3/3
931     debouncing.
932    
933     \begin{figure}
934     \centering
935     \includegraphics[height=2.0in]{kmap33db.eps}
936     \caption{Karnaugh Map Of 3/3 Debouncing}
937     \label{fig:sfrr0:svcn0:00}
938     \end{figure}
939    
940     It can be seen from the figure that the expression for the output is
941    
942     \begin{equation}
943     \label{eq:sfrr0:svcn0:01}
944     ABC + AO + BO + CO = ABC + O(A + B + C).
945     \end{equation}
946    
947     Intuitively, (\ref{eq:sfrr0:svcn0:01}) makes sense---the output
948     will be unconditionally \emph{T} if all three of the most recent samples
949     are \emph{T}
950     ($ABC$). The output will also be \emph{T} if the previous output was \emph{T}
951     and at least one of the most recent samples are \emph{T} [$O(A+B+C)$]---at least
952     one \emph{T} recent sample blocks the output from transition to \emph{F}.
953    
954     Figure \ref{fig:sfrr0:svcn0:01} supplies the C-language
955     code to implement 3/3 debouncing as a vertical mapping.
956     A C-compiler will typically implement this code very directly
957     using the bitwise logical instructions of the machine.
958    
959     \begin{figure}
960     \begin{verbatim}
961     /**************************************************************/
962     /* Assume: */
963     /* A : Most recent sample (i.e. at t(0)), arranged as */
964     /* a group of 8 bits. */
965     /* B : Next most recent sample t(-1). */
966     /* C : Oldest sample t(-2). */
967     /* output : Debounced collection of 8 bits presented to */
968     /* software internals. Note that this is both */
969     /* an input (to the combinational mapping) and */
970     /* the new result. */
971     /**************************************************************/
972    
973     output = (A & B & C) | (output & (A | B | C));
974    
975     /* End of code. */
976     \end{verbatim}
977     \caption{C-Language Implementation Of 3/3 Debouncing}
978     \label{fig:sfrr0:svcn0:01}
979     \end{figure}
980    
981    
982     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
983    
984     \section{Research Interests}
985     \label{srin0}
986    
987     This section enumerates my specific research interests.
988    
989    
990     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
991    
992     \subsection{Mathematical Properties of Timed Automata Systems}
993     \label{srin0:star0}
994    
995     I have interest in the mathematical properties of timed automata systems,
996     including these questions:
997    
998     \begin{itemize}
999     \item Can these systems be rearranged (independent of code generation) for more
1000     efficient implementation? Is there some canonical form?
1001     \item Can an automaton be ``factored'' into components (i.e. the reverse
1002     operation of ``shuffle'' illustrated in Figs.
1003     \ref{fig:staf0:stfw0:00}, \ref{fig:staf0:stfw0:01}, and \ref{fig:staf0:stfw0:02})?
1004     \item Is the factorization unique\footnote{In the same sense that the
1005     fundamental theorem of arithmetic guarantees that a composite
1006     can have only one unique factorization into primes.}
1007     or can it be made unique according
1008     to some metric?
1009     \item Can algorithms spot suboptimal designs and coach
1010     human programmers?\footnote{Example of a suboptimal design:
1011     identical behavior could be achieved using a simpler design.}
1012     \end{itemize}
1013    
1014     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1015    
1016     \subsection{Code Generation from Systems of Timed Automata}
1017     \label{srin0:snvf0}
1018    
1019     I have interest in the mathematics of code generation from systems of timed
1020     automata. One might make the observation that all of the techniques
1021     described in \S{}\ref{sfrr0} are individual and seemingly disjoint techniques that
1022     come about through human ingenuity. I am interested in:
1023    
1024     \begin{itemize}
1025     \item Any unified mathematical framework that includes all of the techniques.
1026     For example, can one find a common framework or way of thinking that includes both
1027     Farey series approximations and vertical counters?
1028     \item Any mathematical framework that, given a smorgasbord of disjoint techniques,
1029     can predict how to apply them to obtain optimal results (this is also
1030     a function of the processor instruction set). (Cost matrices and
1031     least-squares methods come to mind immediately, but I'd like to examine
1032     this more closely.)
1033     \end{itemize}
1034    
1035     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1036    
1037     \subsection{Code Generation and Formal Verification of Properties in the Same Framework}
1038     \label{srin0:sgvs0}
1039    
1040     There seem to be no existing tools that will allow code generation (from
1041     a timed automata model) and the
1042     verification of formal properties in the same framework. In addition, the tools
1043     that do generate code (for small systems) can't optimize as effectively as a
1044     human programmer. With a more sound mathematical basis for optimization,
1045     I believe that tools should be able to optimize more effectively
1046     than a human programmer.
1047    
1048     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1049    
1050     \subsection{Enterprise Content Management}
1051     \label{srin0:secm0}
1052    
1053     I administer web-based version control and defect-tracking databases. This type of
1054     technology is critical because human beings don't deal well with complexity and
1055     there is the inherent need to serialize (one bug at a time, one change at a time, etc.).
1056    
1057     I have some interest in enterprise content management
1058     (see, for example, \emph{Alfresco}), especially the
1059     buy-versus-build dilemma and the difficulty
1060     and cost of developing custom in-house tools that are tailored to an individual
1061     company's processes (I have some ideas in this area).
1062    
1063    
1064     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1065     \end{document}
1066     %
1067     %$Log: phdtopicpropa.tex,v $
1068     %Revision 1.20 2006/03/27 00:10:30 dashley
1069     %Presumed final edits.
1070     %
1071     %Revision 1.19 2006/03/26 23:26:23 dashley
1072     %Edits.
1073     %
1074     %Revision 1.18 2006/03/26 02:22:21 dashley
1075     %Edits.
1076     %
1077     %End of $RCSfile: phdtopicpropa.tex,v $.
1078    

dashley@gmail.com
ViewVC Help
Powered by ViewVC 1.1.25