« December 2003 | Main | February 2004 »
January 27, 2004
[Research] background reading in concurrency theory
[ Concurrency Research - The State of the Art, Classifying models of concurrency] The first is a little dated since it was published in 1996, but seems to cover the high points of concurrency theory. Perhaps useful in getting familiar with the area. The second is less detailed, but offers another perspective on how to classify concurrency models.
It is accepted that there are no good functional models of concurrency. A functional model maps inputs to outputs. Concurrency models begin with a definition of an atomic action. All models use atomic actions and differ in how they "capture the notion of system execution." There are "automata-based" which descibe concurrent systems as "states and transitions between states" and there are "action-based" models which model systems using "structures consisting of atomic actions." An early action-based model was trace theory.
Intensional models "require explicit description of system states and possible state changes" Extensional models "concentrate on the pattern of possible interactions over time".
Interleaving models assume that "observations of system behavior are sequential" so that "parallel actions [are] reduced to nondeterministic interleaving." Truly concurrent models "treat concurrency as fundamental" and system behavior is "represented in terms of the causal relations among events performed by the components of distributed states"
Then there's branching v. linear time. Branching time allows one to track when computational paths diverge.
Either use logical formulas to describe concurrent systems or use an abstract concurrent system to describe the correct concurrent system. Logics are available for branching and linear time specification of correctness (in the form of LTL and CTL, as might be expected). But the differences between interleaved and truly concurrent models remains undeveloped as do the differences between intensional and extensional views of system behavior.
I think our most useful model would be an intentional model that uses interleaved semantics and a branching model of time.
van Glabbeek gives 5 convenient classes of concurrency models.
- graph: like an automata based model.
- net: like petri nets.
- event: a set of events with "some structure on" the set of events that "determines the relations between events" Reminds me of Smolka's intentional models.
- explicit: looks like what Smolka would call a "specification using a system to specify a more concrete system"
- term like CSP or CCS a language with a syntax and a semantics.
Posted by jones at 08:35 AM | Comments (0)
January 20, 2004
[Research] MAGIC: model checking for C
[MAGIC Tutorial, MAGIC home] Of particular interest in comparison with our own forthcoming model checker for C.
Uses predicate abstraction to see if the implementation conforms to a specification. You write the impl.ementation in C, and then the specification is a labeled transition system written in extended FSP notation. The extension is that you can add actions that represent returning an integer value (or void).
Library calls can be handled by allowing stubs that either replace or ignore library calls. This is handy for two reasons: first, you can deal with libraries for which you do not have the source code. second, it is the same work you'd have to do to implement compositional reasoning. So you either get compositional reasoing or ignoring of libraries for free.
Concurrency is managed by listing the names of all concurrent processes in the specification file.
Posted by jones at 12:51 PM | Comments (0)
January 13, 2004
[Education] Eliminating wordiness
[OWL at Purdue University: Conciseness: Methods of Eliminating Wordiness, excercises for eliminating wordiness ] Usefull for both students and faculty.
Posted by jones at 02:10 PM | Comments (0)
January 08, 2004
[Paper reviews] collapsing states
[Model Checking Programs by Willem Visser] Its a very interesting paper from a conference in 2000 (its the 9th entry on the page above). I am most interested in state collapsing.
"The philosophy behind the collapsing scheme is that although many states can be visited by a program the underlying components of many of these states will be the same." (page 4, second column). An example is given for collapsing the rest of a state except the stack frame for a method invocation due to a local variable update.
In our context, the problem is where to draw the boundaries for the "components" in our memory structure.
So I've got just the data segment, code segment and stack collapsed in my little drawing above. The JPF apparently uses components of the program itself. So we'd get into the call stack, variable locations etc and collapse to a finer level of detail. I doesn't make sense to store the ROM, since its, well, read only. I doesn't make sense to collapse the register set or the program counter or the stack pointer. Since they change so often. But it might make sense to collapse the register set. I think empty memory can be collapsed too. Our components are going to be defined at the OS level. So that means we'll know where the data and code segments are, but we won't see into the structure of either of those segments.
See also "State Compression in Spin" by G. Holzmann in SPIN 1997
Posted by jones at 02:10 PM | Comments (0)
January 07, 2004
[Tech Support] iTunes + OS X < iTunes + XP
So maybe I am just a mac newbie, but... iTunes on OS X has be a nightmare. That's ironic because iTunes worked so well on Windows XP. iTunes crashes on my powerbook 2-3 times a day. Not finding anyone else on the web having the same problem, I decide to reinstall it. It turns out that I have to not only delete the progam (by dragging it to the trash, cute, but didn't work) but I also have to delete /Library/Receipts/iTu* (good thing find still works). Of course, I don't know os X as well as I knew XP, so I should cut mac some slack there. But at least the uninstall process that's documented in the XP works.
Posted by jones at 02:09 PM | Comments (0)