Tag: specification

Categories
vy papers

Specifying digital systems using sequential functions

These papers introduce sequential functions for specifying digital systems  like operating systems and networks.  The mathematical basis comes from Moore machines, Moore machine products, and  primitive recursive functions on finite sequences.  Primitive recursive functions on sequences were described by Rózsa Péter  in the 1950s but their connection with automata was not explored. They provide an alternative to state diagrams and other traditional methods of defining Moore machines, and can concisely define very large scale state machines, interconnected machines, and abstract properties of the machines. Composition of primitive recursive sequential functions corresponds to automata products.  The method is aimed at system designs, not verification of program text and is intended as an aid to system designers so that they can understand properties of their systems before writing code.  The first paper is an introduction to the method and includes a number of examples, one of which is a proof that Paxos is safe.

 State machines for large scale computer software and systems

The second paper shows how to use sequential functions define temporal logic like properties – for example, that something is always true, or must become true “eventually”. The sequential function analogs are more expressive – for example, eventually can be made to depend on different types of events and to work with systems that combine components that change state at different rates and in response to different events.

Specifications like temporal logic but with ordinary mathematics

The third paper gives some historical background on automata theory and argues that the 1970s consensus in Computer Science, that classical automata theory is too limited, was incorrect and ignored, in particular algebraic automata theory and automata products. The paper includes a discussion of  “machine homomorphism” introduced in the 1960s, then modified in  process algebra, and then  eventually forgotten in the process algebra and larger formal methods literature. By the mid 1960s, Moore machines and concurrent products of Moore machines were well understood in the automata theory literature, but for a number of reasons, they were not applied to software specification.

Process algebra and automata theory

Also see Digital Circuits as Moore Machines for models of the real-time behavior of simple digital circuits

 

Unlike most Computer Science research on specification, there is no formal logic or other use of axiomatic methods, no lambda calculus,  no non-determinism, no completed infinities (e.g. infinite sequences of events), not even any category theory needed for sequential functions. Then there is a paper defining modularity mathematically in terms of automata products (improving A mathematical basis for understanding software modularity ). And there is a paper that just presents the theory of sequential functions focused on the mathematics, not the CS applications.

The works are released under the creative commons NC-ND  license   with the added condition that use for training or other purpose in Artificial Intelligence systems is specifically prohibited as violating the prohibition on creating derivative works and/or use for profit. 

Categories
academics

The UNIX file system as a recursive function

Ignoring “write” operations, for the moment, a file system is just an implementation, a concrete manifestation, of a map from file names to file contents. A UNIX style file system complicates the story because file names are “paths” through a somewhat compromised tree structure.  You could try to express the relationships between nodes in this tree and paths by brute force axioms. For example: if the path “p” can be resolved to a file, then every proper prefix of “p” resolves to a file that is a directory. But, at least to me, it’s more intuitively compelling to describe the map as a recursive function – capturing the structure algorithmically. In fact, the axiom approach gets pretty damn ugly when we add things like “mounted file systems”.

Begin with a recursive definition of a path: EMPTY is a path and if p is a path and n is a local file identifier then the sequence obtained by appending  n to p (on the left) is a path.  And there are no other paths than the ones that can be built from a finite number of applications of this rule.  We can write “n/p” for the path obtained by appending n to p (appending on the left). Let’s require of course that the separator symbol “/” is not in any local file identifier. Other than that, there is no need to say anything at all about the set of file identifiers now – you can think of it as the set of strings that are “/” free if that helps, but they could be anything at all that is “/” free and can be connected into sequences. And  “/” is just the name we use for the separator, it can be anything at all too.

UNIX style file systems are nearly always constructed on top of flat file systems. That is, we suppose we have a primitive set of “flat file names” of some sort and a map F that maps flat file names to the corresponding file contents.  Flat file names can be the same as local file identifier or different – it doesn’t matter. Right now we don’t have to say much about these flat file names at all but we have some demands on file contents. In particular, files need to be able to “encode”  lookup tables that relate local file identifiers to flat file names. Since we will require that a local file identifier appear at most once in such a table, we can think of the file contents as encoding a function- the “directory function”.  If “i” is a flat file name and F(i) is defined, we need to be able to associate F(i) with a type: plain or  directory (to start). Plain is just some data. If F(i) is defined and F(i) has type directory, there is some function d= D(F(i))  we can decode from F(i) so that for some finite set of local file identifiers, “d” maps those identifiers to flat file names.

The idea is that we can start with some flat file name “i” and a path, say,  p=a/b/c and follow p from “i” as follows. First get i’=D(F(i))(a) if F(i) is a directory. Then get i”= D(F(i’))(b) and i”’= D(F(i”))(c) – assuming that the intermediate flat files are directories and they encode functions that map the flat file names “a”, “b” and “c”.  There’s some complexity because we’re not assured that everything will work out – we may only be able to follow a path partway before coming to a dead end.

So define a function R to take a flat file function F, an initial flat file name “i” and a path p and produces either a terminal flat file name or FAIL if the path cannot be followed all the way.  First we do the easy case R(F,i,EMPTY)= i.  The recursive case is

R(F,i,n/p)= R(F,D(F(i))(n),p) if F(i) is a directory and D(F(i))(n) is definedFAIL otherwise.

Associate F with a special flat file “r” – the root file. Then we can define U(p) = F(R(F,r,p)) if R(F,r,p) is not FAIL and let U(p)= FAIL otherwise.

And that’s it – except that now the flexible nature of the file system becomes clear. Let’s add a new file type “indirect” so that if F(i) is indirect, then we can extract a flat file map and a root flat file name from the contents. That is, if F(i) is an indirect file we can produce (F’,r’) = X(F(i)) where F’ is a flat file map and F'(r’) is a directory under F’.  Say “i” is a properly defined indirect file under F if and only if F(i) is indirect and for (F’,r)=X(F(i)) we have F'(r) as a directory. We can now redefine R as follows to switch flat file systems on an indirect file.

R(F,i,n/p)= R(F,D(F(i))(n),p) if F(i) is a directory and D(F(i))(n) is definedR(F’,r,p) if F(i) is an indirect file and X(F(i))= (F’,r) and F'(r) is a directory

FAIL otherwise.

Note that the first definition of R is obviously primitive recursive – because we lose one element of the path sequence on each recursive step – but it’s not obvious that the version of R with indirect calls must terminate. The final condition on the indirect case assures us that at least every second step must remove one element from the path.

 

Categories
academics

More computer science as humbug [updated with Brazil dream sequence]

Continuing my experiments in academic papers, I sent a paper on automata and circuit verification to CAV2010 (here’s an updated version with some corrections and better references). I actually got one carefully written and well informed review. Sending a paper to an academic conference with no references more recent than 20 years, was probably more of a deliberate provocation than needed, but I’m still amazed at the low quality of the reviewing. First, it’s absurd and frankly shameful that so-called academics can make an unsupported claim that something is well known in the literature. One of the reviewers at CAV2010, was kind enough to write:

There is nothing wrong with the approach described but I fail to see that there is anything novel here either. Circuits have been modeled as state machines since the 60s (e.g. Booth 67), there is a wealth of literature on the correspondence between state machines, automata and strings, and so forth. All of this has been done before, and more completely.

I am sure that one could look in most computer science curricula and find almost all of this material being taught at the undergraduate level.

I’m really embarrassed for the entire profession here. Of course circuits have been modeled as state machines – well before 1967 in fact. Booth’s 1967 book is one of innumerable surveys.  The paper showed an alternative way of representing state machines and illustrated their use on the time sensitive behavior of combinational circuits where they are not usually employed because the number of states is so great as to overwhelm standard methods.  The specific methods used in this papers, as far as I know, are not used elsewhere in the literature – and I still don’t know any different because the CAV2010 reviewer was unable to provide a reference. To me, this is a mark of humbug. Look, if you are going to tell some poor author that their work is retelling some well known tale, you should at the very least be able to point to the well known explications. Creditably enough, CAV2010 offers a rebuttal period for reviews: but even given a second chance, and an explicit request for a reference, both the author of the review and the program committee failed.  An assertion is made that the material is covered in “most computer science curricula” and when challenged, the assertion is just left as is. No wonder so much of academic computer science is mired in stale repetition of old material when basic standards of scientific rigor are discarded by the people who are supposed to be enforcing the rules.

I don’t want to seem entirely ungrateful for the work of the reviewers: one of whom gave a perfectly rational and solid reason for rejecting the paper.

Conclusion: an elegant paper, but doomed for CAV by lack of any attempt at automation or convincing evidence that automation of the methods described would be a scientific advance.

I can’t really argue with that. The paper does not either describe automation or attempt to make an argument of why automation would succeed – although I am in no doubt about the second question. Perhaps the paper is not suitable by reason of the focus of the conference. But of 4 reviews, this reviewer was the only one who appeared to understand the material. One of the other reviewers actually responded to the rebuttal with this:

About the KR theorem and feedback, an ordinary finite state automaton “encodes” implicitly the feedback information of the underlying sequential circuit in its states, so I would be surprised that the theorem is not applicable to digital circuits with feedback

Ok. The KR (Krohn-Rhodes) theory is based on a decomposition called “loop free”. Let me type that again LOOP FREE.  The theory is concerned with the decomposition of state machines into pipelines where components can be ordered so that the output of component i depends only on the input to the system and the outputs of components j<i . What I show in the paper is how to describe one of the simplest and most beautiful achievements of Computer Engineering, a SR-latch via the interconnection of state machines that represent logic gates. The SR-latch is constructed with cross-coupled gates where the output of each gate feeds back into the input of the other gate. When the output of gate G1 feeds into the input of gate G2 and the output of G2 feeds into the input of G1, we have what is known in the technical literature as a “loop”. While the reviewer would not be surprised if a loop-free product could be used to describe a loop,  the comment makes me doubt his/her grasp on the basics of the material (BTW: the identity of this reviewer is known to me, but I’ll leave to him/her to respond or not).

One of the other reviewers included (among others) two comments  that I noted were wrong, but were not modified or defended.

2. The term “propagation delay”: It seems that you blend different concepts into this single term, namely the duration that an input has to be held stable in order to be sure that it will be reflected by the output and the latency of a circuit in forwarding such a sufficiently stable input to its outputs. While your model, by lumping together the two into a single latency, is a conservative approximation of more detailed models, you may want to make sure that your terminology is in accordance with accepted terminology. it.

Here the reviewer apparently does not understand the difference between latch time and propagation delay. Have those definitions changed since I last looked at a digital circuits book? “The propagation delay t_p of a signal path is the amount of time that is takes for a change in the input signal to produce a change in the output signal” (Wakerly, 1990, P 76).

3. The abstraction of your latch leaves the case (set,reset): (0,0) -> (1,1) unspecified, which is fine. You may, however, want to mention this detail in the accompanying text.

Ah well, the second week of Digital Electronics II is not for everyone. “However if we negate both inputs simultaneously, the latch goes into an unpredictable next state and it may in fact oscillate or enter the metastable state.” (Wakerly 1990 P355). See it’s really not so hard to provide a citation.

There’s actually a lot more to ridicule in these reviews – I’ll post more on request, but I do want to look at one more comment from Reviewer4.

I still believe that this paper lacks motivation and new results for being accepted. As the author says himself, the paper is about a technique for specifying automata, and I am not convinced why not doing it directly with automata, using standard and well-studied techniques. For instance, given that the propagation delays of the gates are modeled using discrete time, why embedding them directly into the definition of gates (even underspecified), instead of modelling them directly with I/O finite state machines (or sequential circuits with feedback)?

It’s not at all clear to me what  modeling a gate as a sequential circuit with feedback even means. In terms of digital circuit engineering, a gate is a combinational circuit, not a sequential circuit. The cool thing about a cross-coupled latch is that the feedback produces sequential properties from combinational circuits. So this comment is quite obscure. On the other hand, I/O automata (from Lynch/Tuttle) are a good example of the augmented automata that I’m deliberately avoiding because of their mathematical ugliness. You can take classical state machines and add all sorts of stuff to them: clocks, fairness conditions, oracles depending on the Axiom of Choice, steroids, flavor enhancers, and so on.  The “standard and well-studied techniques” Reviewer4 has in mind are almost certainly timed and hybrid automata which are types of augmented automata. But the argument made in my paper is that the austere flavor of classical automata theory is strong enough to model timing without additives. Rather than responding to this argument, the Reviewer asks why I don’t use the “standard” methods with additives.

It’s certainly possible that the work described in the paper lacks interest to anyone but me ( the “crank” hypothesis). But lacking credible reviews, it’s hard to make any conclusion at all.

A response.

Hi Victor, good to hear from you.

About your CAV paper, don’t get pathetic. Each PC member has to review in a short time numerous papers and he cannot afford the time needed to give full feedback to the author of a paper which shows strict disconnectedness with contemporary verification. Instead of thanking (or even apologizing) to the PC members for the fact that they bothered to read your paper and give you some feedback (one minute browsing was sufficient to predict its rejection) you still complain and make useless noise.

I will send you my rejected paper and its reviews, if you enjoy reading such things.

Pathetic! Ouch.

In other matters

For a variety of reasons, this reminds me of  a conference I attended in Salvador Brazil many years ago which was like something out of a Magical Realism novel involving lachrymose Argentines who longed to teach meringue, drum bands, unbearably tedious talks, dreamlike missed airplane sequences,  a moment when I was sure that Amir Pnueli, his wife, and myself were about to be assaulted while we were discussing the Israeli novel Blue Mountain which according to Pnueli, was set in his home town, random appearances of gigantic fashion models, an abandoned building in which rooster fighting was taking place,  the most delicious beer ever drunk in world history, a peculiar lecture on Fra Angelico and the relationship between New Mexico and Hassidism (“you must look at the white spaces between the words”) , a hero named Hercules, and much more. I returned from the trip to a faculty meeting chaired by Jean Louis Lassez.  Did any of it even really happen? The conference also provided me with an astounding article review: the reviewer explained that I had made an elementary error when I proved something about a set without taking into account the ordering of the set. Even the Baal Shem Tov would not be able to discern meaning in such a comment.

Categories
operating systems

New paper “H2” on operating system semantics

Please see a new version here. I am continuing to try to develop a practical engineering mathematics for operating system and other complex system code.