Home

PDF Version

1. else if now eject playled pauseled stopled Worksitcmd eject 0 0 0 Figure 6 1 Pushlogic Source Code fragment from our DVD player demo given epoch The rule validator must essentially collate the epochs and then check for rulebase consistency in every epoch It can do this as an explicit datastructure but better would be to do it symbolically The tagged fields refer to components of the worldview The other operators all have their normal meanings In the future arithmetic can be supported using Presburger 8 or CVC Lite 7 A fragment of Pushlogic Source for our prototype DVD player is listed in Fig ure 6 1 6 4 Assistance with Network Race Conditions A number of problems arise when a program is distributed over the network and are well known in concurrency theory e g the Dining Philosophers the Byzan tine Generals problem and more general problems in load balancing Any lan guage design must partition the work of solving these problems between compile time and run time and between language level features libraries and application code A distributed implementation of Esterel for instance would still maintain 71 the Esterel concept of the atomic event although there is a heavy penalty in its implementation Esterel does not have a native looser more efficient network paradigm In Pushlogic however the basic operation a write to a remote field is not itself an atomic test and set
2. PL LINEPOINT TREE2 pl assign 1 TREE3 pl diadic YYLEAF pl minus 1 3 exp ss semicolon PL LINEPOINT TREEl pl e as c 1 S stategraph sd id pl formals ss lsect pushl statechartlist ss rsect ss semicolon TREE3 pl stategraph 2 3 5 H pushl_statechartlist nothing LISTEND 0 pushl state pushl statechartlist LISTCONS 1 2 pushl statename sd id 1 s disable mkstring disable pushl state S state pushl statename pl formals ss colon pushl stateitemlist s endstate TREE3 pl state def 2 3 5 s state pushl statename ss colon pushl stateitemlist s endstate TREE3 pl state def 2 0 4 pushl stateitemlist nothing x LISTEND 0 pushl_stateitem pushl_stateitemlist LISTCONS 1 2 i 39 pushl_stateitem pushl statement x implied body TREE2 pl state action mkstring body PL LINEPOINT 51 Sd id ss colon pushl statement TREE2 pl state action 1 PL LINEPOINT 3 S exit ss colon pushl statement TREE2 pl state action mkstring exit PL LINEPOINT 3 pushl statespec ss rarrowl pushl statespec ss semicolon TREE3 pl transition 1 3 TREEO NONE pushl statespec ss rarrowl pushl statespec ss colon pushl statement TREE3 pl transition 1 3
3. exp7 s FQGT exp7 TREE3 pl diadic YYLEAF pl fqgt 1 3 exp7 ss dged exp7 TREE3 pl diadic YYLEAF pl dged 1 3 exp7 exp8 1 exp9 ss stile exp8 TREE3 pl diadic YYLEAF pl binor 1 3 exp8 exp9 8 1 exp8 ss ampersand exp9 TREE3 pl diadic YYLEAF pl binand 1 3 exp9 exp9 ss plus exp10 TREE3 pl diadic YYLEAF pl plus 1 3 exp9 ss minus exp10 TREE3 pl diadic YYLEAF pl minus 1 3 exp10 1 exp10 exp10 ss star expll TREE3 pl diadic YYLEAF pl multiply 1 3 exp10 ss slash expll TREE3 pl diadic YYLEAF pl divide 1 3 exp10 ss percent expll TREE3 pl diadic YYLEAF pl mod 1 3 42 exp11 1 H expll ss_caret expl2 TREEl pl differentiate 2 expl2 1 i expl2 ss hash expl2a TREEl pl wfield 2 expl2a 1 expl2a expl2a ss hash exp13 TREE2 pl raw field 1 3 exp13 1 H expl3 expl3a ss lpar ss rpar TREE2 pl apply 1 NULL expl3a ss_lpar exp_comma_list ss_rpar TREE2 pl apply 1 3 SS lpar exp ss comma exp comma list ss rpar TREE1 pl tuple LISTCONS 2 4 expl3a 1 SS lpar exp ss rpar 2 Ss query exp13 T
4. xml file ss xmql xml qbody ss xmqr xml file 4 xml element 1 i module pushl_def pl_semicolon_opt 1 pushl statement 1 ss_pling bytecode TREE1 pl_compiled_bundle 2 ss xmql xml qbody ss xmqr xml file TREEl pl xml 4 pl semicolon opt ss semicolon nothing H pl_formals ss_lpar ss_rpar NULL ss_lpar formal_comma_list ss_rpar 2 pl actuals Ss lpar ss rpar NULL ss_lpar exp_comma_list ss_rpar 2 pushl_defstyle sd_id 1 s_pebble mkstring pebble H pushl_def s_def pushl_defstyle sd_id pl_formals ss_lsect pushl_decls ss_rsect TREE4 pl def bundle 2 3 4 6 pushl macro decl expl2 ss equals exp TREE2 1 3 pl type Ss lsect value list ss colon value list ss rsect TREE2 pl safeunsafe 2 4 Ss lsect value list ss rsect TREE1 pl unsafe 2 depreciated form S event TREEl pl event LISTEND 0 S event ss lpar value list or nil ss rpar TREE1 pl event 3 s fuse TREEO pl fusetype S lock TREEO pl locktype 36 sa id TREE1 pl tid 1 pushl field decl expl2 comma list ss colon pl type preferred form for now on TREE2 pl fielddec 1 3 expl2 comma list T
5. h A segeuence of two statements g f 3 Assign to f above has immediate effect on this rhs 5 10 6 With Statement The with statement sets up a textually scoped alias for part of tuple space Field references that start with an hash sign inside the statement are refered to this alias An example with devices book xl devices book page number x2 page number x1 and x2 have actually been assigned the same The with statement does not cause sequential composition of its contents 5 10 7 If Then Else Statement The if else statement as found in the C language is supported 5 10 8 Switch Case Default Statement A form of switch statement is supported Multiple tags per statement block are allowed using comma separation Unlike the C language flow does not fall 54 H from one branch into the next and so there is no associated binding for the break statement A tag called default may be used to catch any otherwise unmatched condi tions 5 10 9 Stategraph Statement The stategraph defines a finite state machine where each state has a state name A top level stategraph is always active meaning it is in exactly one state On the other hand a stategraph that is instanced as a child stategraph within a state in another stategraph is inactive not in any state unless its parent is in that instanti ating state A state may instantiate any number of child stategraphs b
6. le ee L lv ee le l lv le ee l The second form is known as an emit assignment 85 10 1 The third and fourth forms are known as integrations 4 6 3 Unilateral Reset to Safe Value Unilateral changes to shared fields can occur for various reasons For instance a device may be disconnected from the network and an application that was relying on it can no longer function As a second instance consider a Pebble that controls the drainage valve on a cistern A Pushlogic script may make the assignment that opens the valve but the Pebble may make autonomous unilateral action to reset the valve to its closed state a safe state once the cistern is empty This is allowed within our definition of a Pebble since the field is stored within the Pebble Local fields will not suffer unilateral changes all changes will accrue from exe cutable rules in the associated bundle 4 6 4 Pushbacks Simple and Complex Undo When an executable rule makes a change to a field that fails a failed update the rule is obliged to compensate with corrective action Otherwise the rule could no longer be viewed also as a universally quantified assertion about the state of the domain The update may fail straightaway or else the field may revert to some safe value after an interval of time Either way the system must perform a pushback after a failure A simple undo involves changing a sensitive parent of the rule to a safe value t
7. age This is the same BDD package as used by the compiler for equivalence checking when it is searching for idempotent closure 85 14 2 The model checker in the compiler can operate on more than one bundle at once checking inter bundle interactions Since the compiler can accept on its command line at most one source file and any number of object files there are three ways the model checker might get invoked e With one source bundle it checks the assertions in that bundle are consistent with the logic in that bundle e With one source bundle and one or more object bundles it checks that the current source bundle will be compatible when run alongside the object bundles in a domain e With a list of object bundles it checks they are mutually compatible The third way enables the compiler to serve as a checker over a set of rehydrated bundles Hence it can serve as the domain checker Scalability is a big problem with BDD based model checking A fair bit of time is used up finding variable orderings that lead to a compact BDD The compiler writes out the order it finally selected to a hidden file odd sm and reads it in again if present in the current directory Since the filename is currently fixed it is important to do widely differing runs in different directories Current research is developing an incremental model checker so that scalability restrictions are greatly reduced 67 5 16 Bundle Meta Info The compiler
8. 1995 cite seer nj nec com kambhampati95comparative html 3 Service Composition for eHome Systems A Rule based Approach M Kirchhof P Stinauer Aachen eHome Group www i3 informatik rwth aachen de tikiwiki tiki index php page ref 1d 206 4 Universal Plug and Play www upnp org 5 Greaves et al The AutoHAN project www cl cam ac uk Research SRG netos han AutoHAN 6 Uwe Glasser Systems Level Specification and Modelling of Reactive Sys tems Concepts Methods and Tools citeseer nj nec com 258 html 7 CVC Lite http verify stanford edu CVCL 8 M Presburger Ober die Vollstndigkeit eines gewissen Systems der Arith metik ganzer Zahlen in welchem die Addition als einzige Operation hervor tritt In Comptes Rendus du I congrs de Math maticiens des Pays Slaves Warszawa 1929 pp 92 101 Bierman and Sewell Iota A concurrent XML scripting language Tech nical Report Number 557 Computer Laboratory ISSN 1476 2986 Iota A concurrent XML scripting language with applications to Home Area www cl cam ac uk TechReports UCAM CL TR 557 pdf 10 Towards Ubiquitous End User Programming Rob Hague P Robinson A Blackwell ACM Conference on Ubiquitous Computing Seattle October 2003 www cl cam ac uk pr publications ubicomp03 11 Lupu E Sloman M Conflict Analysis for Management Policies In 5th Int Symp Integrated Network Management IM 97 San Diego 97 Chapman Hall 12 J Bacon et al
9. Field values can be enclosed in quotes when they need to contain non alphanumeric characters for any reason An integer range is specified with a two dots Elipsis is allowed as an unsafe value represented with three dots Declarations may be introduced with the following keywords input output inout lock local macro and fuse Any number of the same sort may be declared in one statement using commas to separate them Some examples are S05 ml 2 vy 1 2 I E 42 154599 Hs ORI SE Li uetus contented happy sad input atbtcl output a b c2 inout e c3 local david Because Pushlogic is designed to operate in a dynamic extensible environment further values of the fields may occur at run time beyond those defined and checked against at compile time Not every field name needs be declared pro vided the compiler has sufficient information overall to work out the sensitive parent list to put in each object level rule The input declaration defines a field that is only read by the bundle The output declaration defines a field that is only written by the bundle The inout declaration defines a field that is both read and written The writes to an inout field are frequently not explicit in the source code because they arise only during a pushback Definition of a field as input instead of inout can lead to a no suitable sensitive parent setting error from the compiler The local declaration defines a
10. uu og ege eg en thm 1 4 DoPandChecking Granulanty rsen 1 35 RecHydratiotb 2 6 40 tro 5e Ie hat dads C Be ba te eo 2 Ontology 2 1 AGIOSSAIA a o Yo uoa Was uox E AE tee ee a AA 3 Pushlogic Constants 3 1 Atomic Constant Values ob xw Pere pr RE eS 3 2 ByentCoOnstamts xcv eve ee i et ve e da So Pushlogic Types e use act tee sg ke ww aig Ma ade egg Se ae fua 2 3241 LOCK Type i254 cR e REE BES REARS 9 92 USC VBC S qoae eds Bed At a oat deal e d Re d 903 9 Boolean Typer ou v Le tne deri ers ety M eng 4 Pushlogic Object Level VM Execution 4 1 Code Reflection Schema i 2o x 4 2 E cse we obe ey dioe ee dite a s 4 3 Pushlogic Expressions 4 4 Fields and their Declaration 45 Level and Event Expressions oo 20 2 42 o RR 4 5 Syntax directed guide to level and event expressions 4 5 2 Assertions on Level and Event Expressions 10 10 10 11 12 12 14 14 15 15 15 15 16 17 17 19 24 24 26 26 4 6 Executable Rules lees 27 4 6 1 Nominal Meaning of a Rule 24 4 6 20 Event and Level Constraints 27 4 6 3 Unilateral Reset to Safe Value 28 4 6 4 Pushbacks Simple and Complex Undo 28 465 Complex Undo u e AAA oU 29 4 7 Inter Bundle Communication oa oa e 29 4 8 Standing Constraints 29 4 9 Temporal Logic Assertions lt del ERR 33 Pushlogic Source Language 34 5 1 Concrete syntax tree
11. we might want to address all the klaxons on the floor of a building or throughout the whole building Also different Pushlogic bundles might want to use different parallel compositions such that a pair of pebbles that are in parallel from the point of view of one program are separate from the point of view of another There are two basic ways in which a number of pebbels can be addressed at once from a single Pushlogic read or write of a field either the pushlogic code is macro expanded in some way such as being rehydrated more than once or else the pebbles are hardwired in parallel at a lower level such as with additional mech anisms in the tuplecore We require that any pair of fields composed by low level parallel composition have the same tag name and safe value set The meaning of low level parallel composi tion is slightly different for read and write operations We also need to define the behaviour under unliateral change pushback and under message delivery errors When fields that are paralleled are written by a Pushlogic program the writes are simply sent to all of the fields This is useful for instance when wishing to mimic the status of a hardware Pebble with a software GUI that reflects the most recent fields written to the Pebble Each write is sent to each of the two destinations If one of the writes fails or is pushed back to a safe value then the run time system must push back the other fields mapped in parallel a
12. 5 14 4 Compile Time Assertion Checking The model checker constructs a next state relation from the executable rules For the purposes of the relation a hidden input variable is created for every possible pushback which is every safe value of every inout field This is called a pushback input Additional clauses are added to the next state relation to represent that at most one of the pushback inputs of each inout may hold at any one time and that when it holds the variables altered by that pushback have the constant values determined during pushback calculation 5 14 5 Code Output The output code bundle containing executable code field definitions and asser tions is written to four output files that all contain the same information e a bytecode bundle file list of integers in ASCII comma format e a C struct file that contains some initialised C arrays for direct canning into ROM 66 e a dot net version CIL assembly file e an XML encoded version The dot net version can be canned to ROM by compiling it with the ilasm as sembler from the mono project and then using the monos utility program on the resulting bytecode In the future the declarative byte code can also be converted to C to be run as native ROM code instead of being interpreted on the execution platform thereby saving expensive RAM on embedded devices 5 15 Model Checking The pushlogic compiler contains a symbolic model checker that uses a BDD pack
13. Assignments are denoted with the colon equals assignment operator Parallel assignment is supported where the same number of comma separated ex pressions appear on both sides of the assignment e g a b el e2 All executable rules are placed in parallel by default at the top level but sequential composition occurs inside nested blocks unless explicitly written in this parallel form Event and Level Constraints The constraints on the object level assignments between level and event variables and expressions given in 84 6 2 is reflected at the source level but with one relaxation described in 85 10 1 The object level constraints allow the following four basic source forms or any thing tantamount to them if le lv le if le ev ee if ee lv le if le lv ee Rather than assigning to an event variable emitting an event is possible described in 85 10 1 The third and fourth forms are known as integrations 53 5 10 5 Sequential composition Statements separated by a semicolon inside a bundle def mod or top level with with statment are still considered top level and composed in parallel All other statements separated by a semicolon are composed in series corresponding to normal imperative programming An example def bundle s Bundle braces do not force seq a b Three statements in parallel two assigns and an if c e d if e f
14. Condition push back on their support safely so that the rule holds This constraint is stricly stronger than PLC3b PLC3d Safe Live Insertion Constraint An insertion into a DoP that causes an immediate pushback may be considered an error in some applications At least a warning or deferral should be offered to the operative PLC4 Push Back Uniqueness Only one possible pushback procedure should be possible for each possible pushback circumstance If there is more than one then the pbind information is ambiguous The constraint implies that where a parent is shared between multiple rules of a bundle there is just one change to the parent that is acceptable with respect to this constraint for all rules sharing that parent field D7 Undo Race Avoidance Where an undo operates over the network between different execution platforms a race can arise where another independent change to the driven field has been performed by another rule or external agent This normal course of events is illustrated in figure 4 2 whereas figure 4 3 shows the race condition To overcome races a simple undo TBD Needs work Declarative programming languages aim to consist of a set of declarations that all 3This constraint is concave in that two parts of an admissable bundle considered as separate bundles might be inadmissable in isolation 31 hold at all times On the other hand many useful control sequences cannot be expressed entirely
15. ENEE ek ee a ee EE 34 5 2 Abstract syntax tree ets sch ae gd tS eL et ra d Bo eae 44 2 3 Prosram File gots idu a o Sn E CSS Ee M e 46 5 4 Bundle Declaration nit eue cag eee ay ee 46 5 3 Constant Valves v EN ET Eo RC Eee vd gu 47 5 6 Identifiers 4 0 oos e 4 BO ene ee AC MESE PS 47 2 5 Field Declarations X09 ees diuo xe dolo eese RSS 47 SOLL Sor Statement ic ee Bie SE gig Be ee Saks 49 5 7 2 Namespace Binding 2 e eer AT ae ahd as 49 O 5 SR SAU E SUR ROW RASA OR RR OR 50 23 90 Operators iia 4 EE ENEE NI AE Re Ae CE y OE 50 Sek CUR Call 494 Sod pr qe mS 50 5 10 Pushlogic Statements kop s EEN os oo 3 Ae 52 5 10 1 Emit Statement SOAP and GENA too 22 5 10 2 Pebble Statement A uoo ea aa 52 5 10 3 Input and Output Statements 53 5 10 4 Assignment Statement 53 5 10 5 Sequential composition 0 54 5 10 6 With Statement de ip rue ge AG ay ess ts 54 5 10 7 If Then Else Statement 54 5 10 8 Switch Case Default Statement 54 5 10 9 Stateoraph Statement 244 04 sv Soy kop ea n 55 5 10 10 Disable Statement oo 57 7 8 5 11 5 12 5 13 5 14 5 15 5 16 5 17 5 10 11 While For Break Continue Statements 5 10 12 Procedure Call Statement 2 o 5 10 13 Return Statement o LOLA Walt Statement o ad eeu ti A CRUS 5 10 15 Lock Statement coros de ea 5 10 16 PUSE Statem
16. a speech recogniser Each Pebble is able to describe itself using a reflection API such as that provided by UPnP or XMLRPC and register itself with dynamic di rectory services of the form required for ad hoc computing Together with MIT Project O2S we have developed a complete architecture for this sort of behaviour However most importantly no Pebble is able to interact with any other Pebble under its own volition Instead all proactive and interactive behaviour must be held outside the Pebbles in small application scripts that actually cause something to happen For instance consider a DVD player designed to operate with our environment As illustrated in figure each of its major internal components is a separate Pebble at the architectural modelling layer The Keypad Pebble will not make direct contact with the Mechanism Pebble Instead when the play key on the keypad is pressed the application script that glues together the DVD components will convey the event to the Mechanism Pebble to commence playing Using dedicated wiring to carry the output signals as is common practice until now the mechanism will be connected directly to the physical output sockets on the back of the unit Accordingly the application does not have to do anything to convey the multimedia stream to its destination In the future the media will also stream over a packet switched network using a virtual connection It is then the job of the application
17. as a control plane The Push logic sets fields held on media Pebbles such as cameras speakers fileservers and so on to circuit identifier values The Pebbles then send the media streams amongst themselves until again commanded by the Pushlogic If a field naturally ends then its source or destination Pebble can set the controlling field back to its safe value and the Pushlogic receives an undo that can serve in the same ways as a conventional interrupt Asynchronous Eventing Pushlogic may be thought of as an algebra over asyn chronous events and hence has much in common with the work of our Opera group Our fields implement what is now known as a publish subscribe mecha nism The existence of fields is published in the reflection information of a device and they are bound at rule re hydration time When a field changes our wire protocol sends asynchronous notifications to the subscribers 85 Index References 1 A Case for Goal oriented Programming Semantics in System Support for Ubiquitous Computing Workshop at the Fifth Annual Conference on Ubiquitous Computing UbiComp 03 Umar Saif Hubert Pham Justin Mazzola Paluska Jason Waterman Chris Terman Steve Ward http 02s csail mit edu goals html 2 S Kambhampati A comparative analysis of partial order planning and task reduction planning ACM SIGART Bulletin Special Section on Evaluating Plans Planners and Planning agents Vol 6 No 1 January
18. as a process on the target execution platform The combination of the current bundle and all other rules in the domain of participation is model checked If all assertions still hold then the new bundle is acceptable to the domain and becomes part of it Execution of its executable rules is then allowed We also plan to implement a compiler that generates native C code from the bytecode because the current byte code interpreter is RAM hungry and slow 23 4 3 Pushlogic Expressions Pushlogic atomic object expressions are the constant values strings integers and bottom L and the values of fields More complex expressions are built up using operators The operators are any deterministic referentially transparent functions including the normal Boolean connectives and the conditional expression construct query colon The full core set of operators found in Java and C is supported along with string catenation Function calls could be provided for brevity but these are currently fully inlined by the compiler and so do not appear in the object code Expressions are either level or event expressions A level expression is a function of state whereas an event expression will only have a non null value momentarily Arithmetic and comparison operators are provided using the normal coercion rules that allow strings and integers to be interchanged as found in languages such as Perl L is represented with a unique byte code that is disj
19. declaratively For instance when we press the skip forward key on a CD or DVD player we expect it to jump to the next track or index point When we press the button again a new definition of next now pertains and so the operation is not idempotent Implementation of this feature requires both a differentiation to detect the active edge of the button push and an integration to accumulate the increment to the track number PLCS Idempotency Constraint Any Pushlogic program will result in no fur ther output changes if executed more than once without unilateral external change of any field Idempotency is assured if every integration is uniquely associated with a differ entiation In addition an integration of the form a a 1 breaks the Level Ordering Constraint in that a occurs on both side of the rule and hence the level on both sides is equal The solution to this dichotomy is provided by the Gated Update mechanism The gated nature of updates to fields all held on a common platform allows that certain rule combinations to operate deterministically when they would not other wise Consider the following pair of rules where dl is a tightly coupled field di d d2 d amp amp d1 1 1 This pair will reliably set d2 to one whenever d goes from false to true Without the gated update constraint the second rule might always be executed after the first rule and hence the guard would never hold In our current implementa
20. field that is allocated space in the bundle s local tuple The macro declaration defines a name of a subexpression that is macro ex panded before use This might be deleted in future The lock modifier defines a field that supports atomic operations See 5 10 15 The event modifier defines a field that communicates an event See 3 2 The fuse modifier defines a field of Boolean sort that is given low priority for pushback See 85 10 16 The range declaration for a fuse is optional and if provided must be false true When a modifier appears without a preceeding declaration keywork then a local declaration is made 48 5 7 1 Sort Statement The sort set statement associates a user s idenfitier with a pair of safe and unsafe range enumerations It can then be used in declarations as shown in this example sort set mysort s0 sl vl v2 output x b x c mysort inout x d mysort 5 7 2 Namespace Binding All tuples exist in a global name space but aliases or handles for certain points are provided for ease of reference The available handles are denoted with Leading Symbol Meaning dollars Local Bundle Private Namespace lt blank gt Device Platform Namespace hash Device Namespace or with context slash DoP Root tup URI remote tuple access Hash and slash are inter changeable as delimiters between the parts of an heirar chic field
21. pl exp t list pl live of string option pl exp t list pl disable of pl exp t list pl skip pl dv of dv t pl type t list pl macro of pl exp t pl exp t list pl linepoint of linepoint t pl cmd t pl pebble of string pl exp t pi const of string pl exp t pl e as c of pl exp t 45 pl sortset dec of string pl type t pl meta of pl associtem t list pl bundle of string pl cmd t list pl def pebble of string pl formal t list pl cmd t list pl def bundle of string string pl formal t list x pl cmd t list pl facet instance of pl exp t pl exp t pl fun of string pl formal t list pl cmd t list pl stategraph of string pl formal t list pl state t list pl compiled bundle of pl comp t list pl xml of xml t pl filler2 Used only to supress the unused cases warning in my other match traps and pl associtem t pl associtem of string pl exp t and pl state t pl state def of string pl formal t list list pl stateitem t list and pl stateitem t pl transition of pl statespec t pl statespec t pl cmd t option pl state action of pl transitioner t pl cmd t and pl statespec t pl state exp of pl exp t pl exit state exit pl exit state tagged exit of string datatype metainfo t MIA of string string MIA filler eof x 5 3 Program File A Pushlogic Source program is an unordered list of declarations bundle pebble and function definitions A simple program file contains just
22. sleep secs 5 unlocked false wait button local locked unlocked live Door Unlockable Assertion unlocked locked It makes a call to the following timer library function that blocks the thread for a period using the timer pebble provided on all execution platforms As explained there is no notion of thread in the final bytecode because all function calls are inlined during compilation and all thread constructs are converted to executable rule form The live statement is an assertion that the locked variable should never become stuck at one value permanenty 61 fun sleep secs t Local until zs E 02 59 with local timer until time_now second t wait time_now second FQGT until The timer code places the unblocking time in the local variable unt il and then blocks The FOGT operator is builtin and performs a greater than comparison that behaves sensibly as the arguments overflow in their field provided their initial dif ference is less than half the range In the future we would like to use a wider field than seconds 0 to 59 so that we can sleep say for many thousand millisec onds However larger fields consume more BDD primary inputs and BDD nodes which are currently at a premium We shall also consider automatic switching to a lifted form for modelling the sleep call where it is held as a single wait stat ment on a fresh variable This is simpler to m
23. system with its world model can also detect various faults and failures in sensors and actuators and so on A plant world model declaration uses the keyword sequence def world The bundle content is a list of declarations and statements like any other bundle For example def world name input plant heater setting off lo hi Jj output plant ambient temperature 273 forever S al e e lse if lse if leep seconds 1 if setting hi amp amp temperature 90 setting lo amp amp temperature 90 setting off amp amp temperature gt 0 1000 temperature 3 temperature 1 temperature 1 A plant model generates bytecode that does not execute on any platform but which is used for bundle consistency checking The sequence def plant can be used instead of def world to define a world model it makes no difference at the moment 74 Run time checking of the real plant s consistency with world models will be im plemented 75 Chapter 8 Domain Manager The Domain Manager is an aggregation of services that e delimit the domain boundary e manage domain name spaces including network addresses and device names e allow new devices bundles and pebbles to join the domain e fetch canned bundles in respsonse to trigger actions re hydrate them and attempt to insert them into the domain e allocate interpreted bundles to execution platf
24. will not have 65 any consequences on the second or subsequent elaborations After each elabora tion the equivalence checker is used to detect any changes in any symbolic value and if there are then another iteration is commenced Before each new iteration occurrences of _ in the expression for a variable in the environment are replaced with the symbolic value for that variable calculated on the iteration before This exactly models the behaviour of the runtime interpreter which holds or gates all assignments until every subexpression has been recomputed and then performs a commit 5 14 3 Compensation Path Determination After a closed set of symbolic assignments has been computed push back paths are created through the right hand side expressions from any field whose mode is inout For each safe value of an inout field a path is traced backwards through the expression tree that will cause generation of that value These paths extend back though local variables used as intermediate values in any computation For all safe values of all bearing inouts the same path must work for each local vari able This constraint can cause some novel error messages The paths are stored in the push back indication section of each rule Sub expressions are generated by spotting common subexpressions using a hash ing technique Where a pair of rules use a common subexpression this sharing is noted by a re writing phase before code generation
25. 9 on the same device platform hence its name but it can also be used for access to fields shared by other bundles Here we present a simple example using hardwired IP address but actual device addresses should not normally appear in the source code they should be supplied during re hydration def bundle simplelink pebble my_keyboard Pebbles Front_panel Keyboard pebble your_devices tup 128 232 1 10 Pebbles Devices field declarations omitted your_devices front_panel on_led my_keyboard on_switch Pebble aliases can be defined inside a bundle statement as shown or outside 5 8 Pragmas The pragma statment enables control flags to be passed to the compiler These may occur inside a bundle declaration or at the top level of a file See the compiler manual for details of the supported pragmas 5 9 Operators The operators available at source level include all those defined in for object level in 4 3 Each is denoted with its usual symbol or digraph In addition the differentiate operator is provided denoted with uparrow exp The currently available forms are summarised in Figure 5 1 It is our goal to support as many features found in common OO imperative HLLs as possible while still producing output that can be represented as Pushlogic ob ject rules and checked automatically at load time 5 9 1 Function Call Function calls are expanded fully at compile time and so must be have stati
26. Cambridge Event Architecture CEA www cl cam ac uk Research SRG opera projects 13 Monika Solanki et al Introducing Compositionality in Webservice De scriptions Proceedings of 3rd ANWIRE workshop on adaptable services DAIS FMOODS November 2003 Paris 14 Trolltech Creators of QT www trolltech com 15 Paramodulation and theorem proving in first order theories with equality G Robinson and L Wos In D Michie and R Meltzer editors Machine Intelligence Vol IV pages 135 150 Edinburg U Press 1969 16 W3C Simple Object Access Protocol SOAP www w3 org TR SOAP 9 87 Many thanks to Daniel Gordon who implemented much of the first Pushlogic system and who contributed greatly to its definition 88
27. Iinfo type Where there are several pebbles of the same type name on one platform these must have intance names that differ somehow For instance the pusher platform just adds a decimal number on the end of the type_name tup 192 168 1 100 Pebbles ThermalCutout0 tup 192 168 1 100 Pebbles ThermalCutoutl tup 192 168 1 100 Pebbles ThermalCutout2 Platforms also have metainfo This is held using field_names that begin with the word Platform One typical field for a platform is an IP address For instance we would expect the following field tup 192 168 1 100 Platform ipaddress to have value 192 168 1 100 9 0 2 Bundle Metainfo Reflection via Pebble Dataplane Platforms host bundles of running software The local variables and metainfo for such bundles are readable using the pebble_dataplane XML schema Like an instantiated pebble a running bundle has a type name and an instance name and the same naming conventions are used to create instance names as are used for pebbles except the string Bundles is used instead For instance a bundle instance name might be tup 192 168 1 100 Bundles ClimateControl and its metainfo would be stored in fields such as tup 192 168 1 100 Bundles ClimateControl BundleInfo version tup 192 168 1 100 Bundles ClimateControl BundleInfo tcopyrightMessa and its Pushlogic local variables are pl
28. Pushlogic SPLI Language Reference Manual draft Updated January 2007 DJ Greaves University of Cambridge Computer Laboratory April 20 2009 IDavid Greaves cl cam ac uk Abstract SPL1 Pushlogic is a scripting language for a dynamic population of devices e g Sensors processors or actuators and dynamic number of concurrent applications in a reliable or safety critical system It is a constrained language fully amenable to automated reasoning at various granularites It defines re hydration for dy namic binding of rules to new device instances and a load time model checker that runs before a new bundle of rules may join a domain of participation In a typical application of Pushlogic complex embedded devices are partitioned into passive components known as Pebbles API registration and reflection are then used to expose the interfaces offered by the Pebbles All proactive and interac tive behaviour between Pebbles or over the network must then be implemented with Pushlogic and code reflection as we call it exposes this behaviour for au tomated reasoning This report gives the syntax and semantics SPL1 Pushlogic This work was carried out under the CMI Goals Pebbles project 1 This document is currently under preparation and is being changed every month Or SO Contents 1 Introduction D CRoolehanibleW cir 49er xe PAL x nero Palki eee dote Gayle k 1 2 Bundles ad eio abe we take ew eo 1 3 Binding and Naming
29. REEl pl channel read 2 sd number TREEl pl num 1 sd string TREE1 pl_string 1 ss_tilda exp13 TREE1 pl_binnot 2 ss_pling exp13 TREEl pl lognot 2 expl3a sd id TREEl pl id 1 sd string TREEl pl string 1 expi3a ss dot expl3a TREE3 pl diadic YYLEAF pl cat 1 3 ss dollars TREEO pl dollars H se se include lt stdio h gt 43 include lt ctype h gt extern FILE stderr int yyerror const char xs extern builder lishlex extern void exit int extern void givesrcPoint givesrcPoint fprintf stderr Syntax error s Mn s fprintf stderr Next symbol s n atom to str lishlex exit 1 return 1 void yydebug on ifdef YYDEBUG extern int yydebug td yydebug 0 endif char smllib plgram int yylex char s int v 0 extern void givesrcPoint extern builder lishlex extern int lextracef builder xb a lishlex if a return 0 yylval auxval a if fnumberp a return sd number if fstringp a return sd string b fgetprop a smacro if lextracef printf Lex i p s n v b if b return atom to int fcdr b S atom to str a if isalpha s s givesrcPoint cbgerror cbge fatal Illegal input token c return 0 return sd id x eof x ato
30. REEl pl fielddecn 1 depreciated form no type given pushl field decl list pushl field decl LISTCONS 1 LISTEND 0 pushl_field_decl ss_comma pushl_field_decl_list LISTCONS 1 3 pushl macro decl list pushl macro decl LISTCONS 1 LISTEND 0 pushl_macro_decl ss_comma pushl_macro_decl_list LISTCONS 1 3 H case_item S case exp comma list ss colon pushl_statement TREE2 pl case item 2 4 s default ss colon pushl statement TREE1 pl case default 3 case item list case item LISTCONS 1 LISTEND 0 case_item case_item_list LISTCONS 1 2 pl assoclist pl associtem LISTCONS 1 LISTEND 0 pl_associtem ss_comma pl_assoclist LISTCONS 1 3 pl_associtem sd_id ss_equals exp TREE2 pl_associtem 1 3 pushl statement S sort s set sd id ss equals pl type ss semicolon PL LINEPOINT TREE2 pl sortset dec 3 5 ss lsect pushl statement list ss rsect s fuse exp ss semicolon PL LINEPOINT TREE2 pl fused TREEl pl block 2 5 37 s_pragma sd_id ss_equals exp ss_semicolon PL LINEPOINT TREE2 pl pragma 2 4 s fun sd id pl formals ss lsect pushl decls ss rsect pl semicolon opt PL LINEPOINT TREE3 pl fun 2 3 5 s input pushl field decl list ss sem
31. TREE1 SOME PL LINEPOINT 5 H string_option nothing TREEO NONE sd_string ss_colon TREE1 SOME 1 H pushl_statespec exp TREEl pl state exp 1 s exit TREEO pl state exit s exit ss lpar sd id ss rpar TREE1 pl state tagged exit 3 sd_id_comma_list nothing LISTEND 0 sd id LISTCONS 1 LISTEND 0 sd id ss comma sd id comma list LISTCONS 1 3 expl2 comma list expl2 LISTCONS 1 LISTEND 0 D expl2 ss comma expl2 comma list LISTCONS 1 3 exp comma list exp LISTCONS 1 LISTEND 0 exp ss_comma exp_comma_list LISTCONS 1 3 H pl formal exp ss colon exp TREE2 pl formal 1 3 exp TREEl pl formal nt 1 H formal_comma_list pl_formal LISTCONS 1 LISTEND 0 pl_formal ss_comma formal_comma_list 40 LISTCONS 1 3 value sd number ss dotdot sd number TREE2 pl num range 1 3 sd number ss minus sd number TREE2 pl num range 1 3 fprintf stderr Syntax change Please use sd id TREE1 pl id 1 ss ellipsis TREEO pl ellipsis sd number TREEl pl num 1 sd string TREE1 pl string 1 value list
32. aced in tup 192 168 1 100 Bundles ClimateControl Locals varl tup 192 168 1 100 Bundles ClimateControl Locals var2 80 Chapter 10 Execution Platforms A number of execution platforms are envisaged but they share the same API when viewed from the network Currently there is an interpreter for the bytecode in the badger pushlogic directory that can be compiled for embedded systems or workstation use When compiled for a workstation it is called pusher A native compiler for the CAN PIC platform is also planned has been envisaged The pusher interpreter may also pretend to be an execution platform pebble mean ing that it might beacon some metainfo so that a domain manager gives it some bundles to run Currently all platforms speak the ETC protocol over the network There is a utility called cmdline that enables one to manually send low level ETC commands over the network The cmdline program allows platform reboot and field read write and subscribe operations Arg syntax 1s cmdline nNONCE pNNN dURI reboot cmdline nNONCE pNNN dURI w tag v tag v cmdline nNONCE pNNN dURI r tag cmdline nNONCE pNNN dURI s tag For example to change the value on the display panel pebble one can use some thing like to set a remote field cmdline d tup 169 254 25 193 253 w Pebbles Display value Hello Wc Several field value pairs can be supplied to
33. ad time but as far as possible are also implemented by the compiler to give ad vanced warning 5 1 Concrete syntax tree The concrete syntax tree is following yacc file Id pushlogic yy v 1 35 2008 07 11 08 15 04 djg11 Exp Bigtop CBG Badger Tuplers Project University of Cambridge Computer Laboratory C 2004 David J Greaves Mostly Written Romsey Dec 2004 4 Ok Oo db db SE db db db db OR x 0k ox Pushlogic Grammar 34 t include cbglish h include lt stdio h gt define PL LINEPOINT X add linepoint pl linepoint X D P P oe union builder xauxval stype type type type Stype type type type type type se se prog lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt lt auxval gt pushl_decls pl_assoclist pl_associtem bytecode pushl_decls prog module value value_list value_list_or_nil pushl_def pl_formals pl_actuals pl_formal pushl_defstyle pushl_statement pushl_statement_list case_item case_item_list pl_type pushl_statename pushl_statechartlist pushl_state pushl_stateitemlist pushl_stateitem pushl_statespec sd_id_comma_list pushl_field_decl pushl_macro_decl pushl_macro_decl_list pushl_field_decl_list exp expl exp2 exp3 exp4 exp5 exp6 exp7 exp8 exp9 expl0 expll exp12 expl2a exp13 expl3a string option formal comma list exp comma list expl2 comma list xml file xm
34. ained controlling language called Pushlogic Pushlogic object level is a byte code designed as an inter mediate code for automated reasoning with respect to several execution models that vary in how fast a program can be checked and how accurately effects of message loss or delivery delay are included Pushlogic source level looks like an unconstrained imperative multi threaded OO like language where the partition ing between decidable and undecidable constructs is not immediately apparent to the programmer Pushlogic object consists of bundles containing rules Rules are either consis tency assertions expressed in temporal logic or else executable rules that define a finite state machine or mechanism Bundles run inside a domain of participa tion DoP Dynmaic storage allocation only occurs when new bundles of rules are loaded into a running DoP Bundles arrive either when a new pebble that requires control arrives or when a new application is started expressed in Pushlogic Be fore a bundle can be loaded the union of the rules in the new bundle is formed against those already in the domain If any of the rules are inconsistent or any of the temporal logic rules existing or new will not hold under the combined mechanism the bundle cannot be loaded Pushlogic is a finite state language but the amount of state in a Pushlogic domain varies over time as new bundles or pebbles enter and leave the DoP Instead of being executable a
35. al variables in a tuple called Local 69 PAE 6 3 Pushlogic Timer Every Pushlogic platform provides access to a timer The timer has a real time clock and also provides any number of countdown timers The local real time clock may be accessed by first declaring the following fields in the Pebbles tuple of the local platform and then reading them as needed input Pebbles Timer Timenow hour 0 23 Pebbles Timer Timenow minute 0 59 Pebbles Timer Timenow second 0 59 If the local bundle also sets the real time clock then it should declare these fields using the inout keyword Countdown timers are created by declaring a field inside Timer Countdowns Two different bundles on the same platform will interfere if they both declare the same count down counter this needs blocking The field must be set to an integer number of milliseconds and it counts down to zero by itself The following code fragment illustrates how to make a light flash at five hertz inout Pebbles Timer Countdown mytimer 0 100 output Somedevice lights light off on with Pebbles Timer Countdown if mytimer 0 mytimer 100 Half cycle every 100 milliseconds if light on light off else light on The rest of this section is obsolete Frequently rules must fire at a particular time of day or describe constraints that apply only for specific periods of time Examples are respectively Turn t
36. allowed to commence execution and may also be re hydrated before checking A bundle contains rules and meta information 1 3 Binding and Naming Bundles have access to several namespaces 1 Their own local name space 2 a namespace local to the platform they are running on 3 a namespace local to the domain of participation DoP 4 a global or outermost namespace accessed via URIs 1 4 DoP and Checking Granularity A Pushlogic program executes in a domain of participation DoP A DoP typ ically encompasses some number of Pushlogic execution engines DoPs may become merged or federated as explained in section 8 3 Various agents may attempt to insert a bundle into a domain of participation For instance a starting bundle may be loaded by the agent that first set up the domain Equally when new devices are added to the system an associated bundle is also typically of fered The presence of certain combinations of pebbles and bundles in a domain 10 may trigger loading of further bundles eg a fire alarm system might be automat ically implemented whenever there both a smoke sensor and an alarm klaxon are present in the domain A bundle must be checked against all other rules already in the domain and if all rules hold then the bundle joins and its rules start to take effect as well A bundle may also be unloaded by deleting all of its rules at any time provided it is not critical to ensuring a consistency rule that is n
37. an unsafe value or to prevent a field from being externally set to a safe value See also 84 6 3 The internal reactive behaviour of a Pebble is described currently using Pushlogic rules that have their own schema described 4 1 9 0 1 Platform Metainfo Reflection via Pebble Dataplane An instantiated pebble sits on platform which is either an embedded system or server In terms of registration and metainfo platforms have the same structure as Pebbles and hence do not show up as an explicit structure in the XML schema A platform has a platform name that is a globally unique list of strings of which the first might be a URI string ie has the prefix tup For embedded system platforms quite frequently there is only one instance of a given pebble ever present on the platform and because all execution platforms have unique names the plaform s name can be extended with the string Pebbles and then the pebble s type name is appended on to that to form the unique instance name for the pebble 19 For instance we might have a platform called tup 192 168 1 100 and a pebble type name of ThermalCutout giving a pebble instance name of tup 192 168 1 100fPebblesfThermalCutout The metainfo for this example pebble would be found at tup 192 168 1 100fPebblesfThermalCutout lI nfo and we would expted the following field to also have the value ThermalCutout tup 192 168 1 100 Pebbles ThermalCutout
38. and and Compile Temporal Assertions NULL ENV Create Binary mme Encodings Repeat Parallel until Elaboration closure Equivalence BDD Checker Package Pa vo a 7 1 ge M FA vf 7 1 Executable 7 3 Rules E d 1 Subexpresion Model Sharer Checker Consistency i Checkers FAIL BEE EEN Compile ki Convert Time tc Assert A Lage Failures Bundle File Native Code Figure 5 2 Internal structure of the Pushlogic Compiler in the source code a section of I code is generated I code consists of labels go tos waits assignments and conditional branches For each section a run time program counter is defined At the object code level these program counters act just like other local variables and their values range over the labels in that sec tion There is no run time spawning or joining of threads although the illusion of this can be provided from a static set of threads using pre processing techniques Temporal logic assertions in the source code are split off and held separately Liveness assertions may be guarded by nested if statements and by the current value of the program counter Each I code instruction is stored in an array indexed by compile time program counter and each has one of the following forms x Intermediate imperative assembler code form zi and icode_t I assign of bc t be t I resultis of bo t I goto of int I
39. and hence we need to consider the further support required to avoid problems from network races and unreliability Any program that contains a race of the nature shown in figure 4 1 will not unwind during compilation since the final result depends on the order of interleaving Races As fields are names in a global name space there may be network delays in making access to their values for read or write Races may also arise in that no synchronisation between reads and writes is implemented at execution time The binding part of resource allocation is handled in Pushlogic at re hydration time All instances of a given type of device must be given unique identifiers dur ing binding and because currently there are no arrays in Pushlogic each identifier must textually exist in the Pushlogic source program 6 4 1 Test and Set Facility Consider a pair of DVD players that are commanded at once to send their output to a single display where that display can only handle a single stream If the display has a field that says which stream it is currently receiving then the most simple form of resource allocation is to allow this to set at any time and the most recent write to it is the current winner This gives the familiar radio button method of source selection Where it is important that a resource is claimed for a specific interval terminated by an explicit release then concurrency theory tells us that an atomic test and set is required at s
40. bundle may be a plant bundle that models reactive and autonomous behaviour not programmed using Pushlogic A world model mirrors the behaviour of the physical system or plant or other software agents In many real systems there are predictable effects from the output of actuators that may be detected by sensors These feedback effects can cause undesirable effects such as deadlock or oscillations that Pushlogic can detect before they occur Run time monitoring of the conformance of the real system with its world model can also detect various faults and failures in sensors and actuators and so on We use the term mechanism for our combination of FSMs because it models not only the effect of inputs on outputs and internal state but because a mechanical system of levers and cogs can sometimes be operated in reverse with pressure applied to an output causing an input to change Pushlogic implements a form of compensation where rules are executed in reverse This is called a pushback We believe this greatly reduces the effort required to handle errors and failures To start with less code needs to be written but the real win is that error recovery procedures then add little overhead to the automated rule checking Pushlogic runs on real platforms under its own interpreter or compiled to native code or in one extension to net bytecode Two main execution platforms have been developed a unix workstation application called pusher that a
41. cally bounded recursion 50 String constants quotes optional if part of an enum e g hello Local hierarchic field names a b c Remote hierarchic field names tup 128 232 1 22 attbitc Function call f a b c Vector of expressions Comparison predicates lt gt lt gt fos Integer arithmetic Differentiation exp Conditional expression g S Sy Blocking remote procedure call e g rc device String catenation operator e g nice g 1 rl S Attribute access with constant tag string e g var ID Figure 5 1 Pushlogic Source Operators 51 5 10 Pushlogic Statements 5 10 1 Emit Statement SOAP and GENA too The emit statement delivers a Pushlogic event This may be mapped to a non Pushlogic GENA event or device RPC during rehydration 5 11 1 if ee emit event name if ee emit event name args The emit statement is shown in the context of an if statement that is guarded by an event expression Such a guard must normally exist within the surrounding program flow control in some form or another If the guard is a level expression this would allow cause a nominal continuous stream of back to back events to be emitted and would tend to violate idempo tency The guarding context may be a level expression if the event being emitted is en tirely local and the nominal stream of events is local to t
42. ccordingly These push backs appear as undo s to code in other bundles that drives the mapped fields and to new writes to code that references the mapped fields For fields written unilaterally by external devices or fields that refuse to accept a pushback the value of their parallel composition is defined to be the most recent value written to any one of the fields This provides suitable behaviour when a number of very simple push button pebbles are paralleled the push logic program receives the up and down strokes of each key with no demarcation as to which button was pressed However it is expected that even the most simple push but tons whether implemented physically or as part of a GUI will be momentary at the point of operation but with built in status indicators as latches and therefore able to accept a push back If the off state is safe and the on state not then and any pushback to off will turn off all the indicators These ideas extend easily to other forms of widget 73 Chapter 7 Plant Model Instead of being executable a bundle may be a plant model A plant model mir rors the behaviour of the physical world system or plant In many real systems there are predictable effects from the output of actuators that may be detected by sensors These feedback effects can cause undesirable effects such as deadlock or oscillations that Pushlogic can detect before they occur Run time monitoring of the conformance of the real
43. ctual variable field tuple references A soft pebble is one that can run on any networked execution platform It has no specialised or associated hardware A device contains Pebbles and Bundles execution resources and other sys tem services that are neither Pebbles or Bundles A service is the same as a device However the term is used for software only devices These can generally be dynamically instantiated whereas hardware devices are instantiated by a user introducing one into the domain A DoP is any space in which a quantifier ranges Typically this covers a physical or logical space Most trivially it is the local UDP broadcast sub net An example use of a DoP is a rule which says all lights must be off when the master switch is off in this example the word all is interpreted 12 with respect to the current DoP Devices and Pebbles can participate in sev eral domains at once Atif is working on this 13 Chapter 3 Pushlogic Constants Pushlogic source and object use the same constant forms 3 1 Atomic Constant Values The constant values available are integers and strings Strings that are defined as part of an enumeration or the reserved strings true and false do not need quote marks when they appear at source level but at object level there is no concept of whether a string was in quotes or not at source level Constant value strings containing spaces must be enclosed in quotes at t
44. e FALSE and 0 An instantiated pebble is the conjunction of an instantiated pebble and an in stance name The instance name is a globally unique list of strings of which the first may gen erally be a URI string ie has the prefix tup The field names of an instantiated pebble are logically assimilated into the global address space by prepending the instance name The pebble information metainfo for a pebble is held as part of the pebble dataplane as fixed value fields with pre assigned field names whose first element is info Therefore there is no specific part of the pebble XML schema that corresponds to metainfo These fields have read only type their domain safe list consists of a single string that is identical to their fixed value their unsafe domain list is empty Most of the metainfo is missing until a pebble is instantiated but the type name should be present in the field with name Info type Pebbles do not act on other pebbles but can have internal reactive behaviour in the form of various unilateral interlocks and releases For instance a hardware interlock may prevent a furnace control field to be set to ON if a thermal cutout field is registering OVERHEAT This is an example of an interlock An example of internal reactive behaviour would be if the pebble set its own furnace control field to OFF when the thermal cutout field is reading OVERHEAT None of the internal reactive behaviour is allowed to set any field to
45. e held as server state and part of it can be done later for instance to bind to other devices encountered in the domain at run time Ubiquitous computing architectures such as those based on XML UPnP and XMLRPC have matured in terms of their support for automatic registration in directory services and description of the command APIs offered by devices for asynchronous eventing and RPC However until now there has been little empha sis on automated description of the proactive behaviour of applications running in such an environment These applications invoke operations at various APIs available on the local device or over the network Without these applications the APIs would remain unused and pointless However when dozens of applications are running at once in an environment like a home car or hotel room they are bound to interact and occasionally disagree about the current correct setting of some value such as brightness of room lights or locked state of a door A solution to this problem is being explored within our AutoHAN project 5 In our approach each device must be architecturally componentised into some num ber of passive Pebbles and a set of Pushlogic rules that control these Pebbles A Pebble can represent a fairly large chunk of functionality it could be a hard ware component such as a wall mounted keypad or a fire alarm sounder or it could be an entirely virtual device hosted somewhere on the network such as
46. e inout variables hall light and hall Switch can be changed by the user as well as by a Push logic program Program counters and other local variables are stored in tuples held under the Local tab in a unique sub tuple for each bundle instantiated on the platform We also have a locally written universal UPnP control point that can perform roughly the same function for a subnet of UPnP devices We will shortly merge the functionality of these two GUIs The GTK GUI allows the user to view and manipulate the TupleCore tree in real time It uses the tuplecore library to access the TupleCore and it needs a function get domain which is included in the PushLogic library It needs to be initialized using init gtk and gtk tree root tup NULL builds the user interface A 82 S7 outside Y hall gt Bundieinfo outside lantem hall light gt Local off off Y mains hall Switch mains supply off v off v inout hall light foff on output outsidetlantern off on3 input mains supply toff 1 on inout hall Switch toff oni local light on 0 1 13 local light not on 1 03 light on lt hall Suitch on amp amp mainstssupplu on light not on 1 light on outsidetlantern t light not on off 1 on hall light t light not on off on Figure 10 1 Lanterns An Example of Pushlogic under GTK GUI thread needs to be created which runs do_g
47. e same wait statement while the condition still holds the thread is not blocked Where more than one wait statement exists for a thread a program counter vari able is created and stored as a field in the bundle s local tuple 5 10 15 Lock Statement The lock statement declares a field that supports atomic test and set operations A field of sort lock has as its safe value the empty string 58 Any bundle may store a value in a lock field but only if it is currently null If it is not null the write will fail and a pushback occurs A bundle typically stores its own private identifier accessible from the metainfo tuple 86 1 A bundle is responsible for clearing the lock back to the empty string when it has finished with the guarded resource 5 10 16 Fuse Statement Where a section of code does not intrinsically support a push back operation it may be associated with a fuse variable by enclosing it in a fuse statement For example consider the following invalid code input X x S US inout Y y S US Ys X The problem is that if Y Z y makes a unilateral change from US to S which it is free to do since it is an inout then no push back is possible because Xfx is an input that cannot be changed from inside the bundle The solution is to enclose the rule inside a fuse This fuse is able to blow should Y y make a push back input X x S US inout Y y S US fuse Fl
48. ent lt uox uox daa sd AAA Pushlogie RPC ad ead a Bee ke a Re aed ae 5 11 1 Foreign RPC SOAP and GENA SUL Native RPC as a alal ah eee Be Sree ERU OO Structures A vx rx EE OE OE BE X Temporal Logic Assertions 0 2 eeuu ms Compiler Operation 2 40244 54258 2k Re kud bi kt 5 14 1 ConversiontoI Code 5 14 2 Repeated Elaboration from each Entry Point until Closure 5 14 3 Compensation Path Determination 5 14 4 Compile Time Assertion Checking 5 14 5 Code Output pass my rende ra PW Model CHECKING aia wee qoe revo derer Peer ee KE Bundle Meta Info a See ed Mee SES BES EE E R Binding HOOKS 4 aue dcm A oe ate aoe ae Ahan ee a ns Standard Environment 6 1 6 2 6 3 6 4 6 5 B ndl Meta Info d 2544 gom eode qe qua date Local Variable Store oe oe aa Y Rs Rusblopic ASE i i uod oe v ee SE eS SS Assistance with Network Race Conditions 6 44 1 Test and Set Facility 0 44 44 tu o ee 6 4 2 Make break Issues 4000 x es xe 9 dele x ACORN Low level Parallel Composition of Tuples Plant Model Domain Manager 8 1 Using the compiler to check domains 64 66 66 66 67 68 68 69 69 69 70 71 72 72 73 74 76 8 2 Incremental and Real time Model Checking 8 3 Federation of PushlogicDoPs 9 Pebbles and Pebble Formal Model 9 0 1 Platform Metainfo Reflection via Pebble Da
49. es not appear in the object code it serves only to influence the push back information 4 6 5 Complex Undo The complex undo is expanded at compile time using extensions of the fuse statement No object level representation is needed 4 7 Inter Bundle Communication All communication between entities is through shared variables Multimedia is supported using the notion of third party setup where a field in a source pebble is set to the same value as a field in a sink pebble where the value acts as a virtual circuit identifier Where a bundle alters the value of a field held on a remote resource the run time system generates network traffic such as a SOAP RPC 16 Where a bundle is sensitive to changes on remote resources it uses a soft state registration protocol a UDP version of UPnP s GENA that causes it to receive notification of changes An inout field may be set to one of its non safe values by at most one bundle Changes in local or remote field values are notified to the Pushlogic execution engine because it registers for appropriate notification callbacks v exp 4 8 Standing Constraints Apart from embedded safety and liveness constraints coming from bundles every DoP is subject to the following standing system constraints A bundle cannot be loaded if it would violate any of these constraints PLC1 Level Ordering Constraint For every rule the level of the assigned field must be less than any level fou
50. f Sequential Composition Sequential composition of statements is implemented by forming a conjunction of their translations but where any assignment is implemented as as symbolic substitution before translating a next statement v e Ca gt vu el A C e v C1 C x Ci A C Elaboration of WAIT The wait statement essentially divides an infinite thread circuit into a number of arcs Each arc commences with a different setting of a synthesized program counter that is generated for each parallel statement containing waits These pro gram counters are stored in the local tuple of the execution platform and renamed to be unique at bundle load time The program counter may be set to one of a number of new values at the end of each arc depending on conditional execution paths within the arc A program counter must be classed as integrator its next value depends on its current value The guard conditions present in wait state ments must accordingly somehow achieve the differentiator property when the bundle is model checked as a whole Some examples will be added here Elaboration of IF THEN ELSE The if then else construct is converted to an object form conditional expression if c then T else F c T F that is then expanded as usual c t f gt c t V c f After the first elaboration from all entry points the process is repeated using the environment created by the first Code guarded by differentiators
51. fecount use required type xs integer gt lt xs complexType gt lt xs element gt lt xs element name PK_ellipsis gt lt xs complexType gt lt xs element gt lt xs element name PK_fieldd gt lt xs complexType gt lt xs choice gt lt xs element re K_fielda gt lt xs element ref PK_tup gt lt xs choice gt xs attribute name argls use required type xs NCName gt lt xs complexType gt lt xs element gt lt xs element name PK_rule gt lt xs complexType gt xs sequence xs element ref PK fieldw lt xs choice gt lt xs element ref lt xs element re lt xs choice gt lt xs element maxOccurs unbounded ref PK_skip gt lt xs sequence gt lt xs attribute name timer use required type xs integer gt lt xs complexType gt lt xs element gt lt xs element name PK_fieldw gt lt xs complexType gt xs sequence xs element ref PK fielda lt xs sequence gt xs attribute name argls use required type xs NCName gt xs complexType xs element lt xs element name PK tup lt xs complexType gt lt xs attribute name argltup use required type xs NCName gt lt xs complexType gt lt xs element gt lt xs element name PK_fielda gt lt xs complexType gt xs sequence xs element ref PK tup lt xs sequence gt xs attribute name argls use required type xs NCName gt lt xs complexType gt lt xs element gt lt xs e
52. generates a small amount of meta information and stores this in a dedicated tuple in the local space 5 17 Binding Hooks Before execution and insertion into a DoP a bundle is re hydrated using operations akin to macro language rewrites 68 Chapter 6 Standard Environment Pushlogic programs may rely on the presence of certain libraries at compile time and certain Pebbles at run time 6 1 Bundle Meta Info Object code from the compiler automatically contains assignments to a tuple called BundleInfo This includes meta information regarding the compiler ver sion source file name and so on Code in the bundle may also typically store additional meta info for example BundleInfo Company Acme Limited BundleInfo Release Version 21 2 The execution platform stores the BundleInfo tuple in the local tuple for the bun dle The local tuple is stored in the Bundles tuple of the hosting execution platform under a field name that serves as a unique instance identifier for the re hydrated bundle Additional information can be passed to the BundleInfo tuple using the meta statement This statement takes a comma spearated list of tag value pairs For example meta Subassembly Motioncontrol Release Version 21 Currently the meta statement does not do anything other than create a field in the BundleInfo and store a constant expression in it 6 2 Local Variable Store Pushlogic places its loc
53. h question is it a good idea that the rules for rehydrating bundles to be implemented in the same language that is used within the bundles themselves How do they need to differ and why One clear distinction is that Pushlogic SPLI is a finite state language whereas dynamic rehydration changes the amount of state This separation might be also most helpful in maintaining amenability to automated correctness checking In the future we may define forms of Pushlogic that are not called Simple Pushlogic These may support dynamic state creation e g to implement RPC server sides 11 Chapter 2 Ontology The and 2 1 Pebble Bundle Canned Bundle Soft Pebble Device Service Domain of Participation Pushlogic approach defines its own ontology This covers device structure also domains of participation Glossary A pebble is a basic entity that can register its existance in a domain broad cast events and be controlled over the network A pebble does not interact directly with any other pebble A bundle of Pushlogic rules consists of software temporal logic assertions and meta information It may be interpreted by a Pushlogic exection plat form or be natively compiled It is the only class of entity that provides communication between Pebbles A canned bundled is stored in a file on a server or in ROM ready for re hydration It may contain formal variables that are replaced in macro expansion style to a
54. hat again makes the rule hold when viewed as an assertion An undo must also be performed by the rule if another rule or an external agent changes its driven field Push back information must be provided where there would otherwise be more than one possibility for compensating If an external agent or other rule changes the value of the assigned field to one of its safe values the push back indica tion uniquely identifies fields occurring in the associated expression that can be changed to make the rule hold For information loosing operators values must also be provided For example with logical not no indication is required be cause the new value is obvious at push back time For comparison when pushed back so it holds then it is sufficient to specify one operand to push back on since it must be pushed back to the current value of the other operand For compar ison when pushed back to false a value and operand must be specified since in general there are many possible vaues that will make a comparion fail For 28 conjunction when pushed back to false knowning which operand to push on is required since either will do whereas to push conjunction to hold may require both its arguments to be changed For the conditional expression operator the condition may have to be changed and also the value of that side of the operator may have to be changed The pushlogic source cut function or whatever it is currently called do
55. he current bundle and is integrated back to being a level expression in all places where it is used In the future it is envisaged that closer integration with UPnP SOAP and other device control languages will be implemented and hence the emit statement will be implied by constructs such as if ee house livingroom curtains setto halfway This need arises since many devices have an event driven API and integrate the received event stream to set their internal state these are conventional models of commanding over an asynchronous packet network 5 10 2 Pebble Statement The pebble statement is used to hard code the address of a network resource such as the IP address and port number of a remote pebble This statement should not normally be used and should not occur in portable code Binding is normally performed at rehydration time mapping symbolic constants in the source code to active network addresses def bundle displayecho pebble PushClock tup 169 254 25 32 1200 input PushClock Pebbles ClockDisplay Leds hour 0 22 zo input PushClock Pebbles ClockDisplay Leds minute pebble DisplayPanel tup 169 254 25 192 1202 0 59 output DisplayPanel Pebbles Display value No message yet Use the string cat operator dot to make the output message value Time now hour minute 5 10 3 Input and Output Statements 5 10 4 Assignment Statement
56. he light on at 6 30 pm and AII lights must be off between 01 00 and 06 30 As a basis for execution of temporal rules a clock device is provided as a local resource at each Pushlogic interpreter At the object level it accessed in the same way as any other Pebble but hooks for handling time are built in to the Pushlogic source language Time encompasses both a linear infinite sequence and a set of finite periodic schedules hourly daily and weekly We refer to each of these as a base temporal extent Any constant time expression mentioned in the rules can be seen as a partition of a base temporal extent into two temporal extents or epochs before the mentioned time and after the mentioned time Taking the union of all partitions on temporal extents leads to a finite number of epochs It is simple to statically evaluate whether any expression referring to time is true or false in a An exception is that if only one time expression exists and it refers to a periodic temporal extent then it has no effect 70 with Pebbles Keypad if now stop playled pauseled stopled Works cmd stop 0 0 1 else if now play playled pauseled stopled 1 0 0 Workstcmd play else if now pause amp amp local keypad_old pause if Works cmd play playled pauseled stopled Works cmd pause 1 1 0 else playled pauseled stopled 1 0 0 Workstcmd play
57. he source level They should be avoided for everyday device control Integers are rendered in base ten and have no leading zeros except for zero itself In all respects an integer behaves equivalently to its corresponding base ten string The runtime system e g Pushlogic interpeter may freely convert between ASCII string and binary representations of integers as it wishes Pushlogic object also uses the special constant bottom also known as backstop 1 The null string the string false whether in quotes at source level or not the integer zero and any strings containing only zeros are the values that represent logical false in the evaluation of Boolean operators The null string is defined as the string of length zero There is no separate null pointer version of the null string and string variables cannot be null Any plat form that uses the null pointer to represent the null string must ensure the two are fully identified under comparison and so on 14 3 20 Event Constants Certain fields or variables range over events The event name is the same as the name as the field or variable that relays it Events may be parameterised with an event constant that is a string or integer An event type is a set of unique strings and or integers that are the event constants possible for a given event The null event constant denotes that an event is not currently occurring 3 3 Pushlogic Types Types in SPL 1 are sets conta
58. iate Each assertion can have a textual name A live assertion asserts that a condition must reoccur infinitely often A never assertion asserts that a condition must never occur An always as sertion asserts that a level condition must always holds and is equivalent to a never statement with negated condition In these assertions any number of condi tions may be listed separated by commas and these have the same meaning as if provided in a separate statements Live statements may occur inside if then else and other control flow statements in which case each condition is guarded by conjuncted with the enclosing conditional statement guards In the future these simple assertions will be augmented with richer assertions that span the ground between liveness and safety i e until assertions and assertions that specify quantitative maximum and minimum valuations on resource use always string exp exp never string exp exp live string exp exp The string is the rule name that is carried forward for output by logging or moni toring code We illustrate liveness checking using the following bundle that causes a variable called locked to be false for 5 seconds after a variable called button holds def bundle ButtonLock f input v keys button false true output v locks unlocked false true forever wait button unlocked true
59. icolon PL LINEPOINT TREE2 pl dv TREEO dv input 2 s lock pushl field decl list ss semicolon x PL LINEPOINT TREEl pl lock 2 s_output pushl_field_decl_list ss_semicolon PL LINEPOINT TREE2 pl dv TREEO dv output 2 S inout pushl field decl list ss semicolon PL LINEPOINT TREE2 pl dv TREEO dv inout 2 S local pushl field decl list ss semicolon PL LINEPOINT TREE2 pl dv TREEO dv local 2 S facet exp ss equals exp ss semicolon PL LINEPOINT TREE2 pl facet instance 2 4 S macro pushl macro decl list ss semicolon PL LINEPOINT TREEl pl macro 2 S const sd id ss equals exp ss semicolon PL LINEPOINT TREE2 pl const 2 4 S pebble sd id ss equals exp ss semicolon PL LINEPOINT TREE2 pl pebble 2 4 S with exp pushl statement PL LINEPOINT TREE2 pl with 2 3 S skip ss semicolon PL LINEPOINT TREEO pl skip S break ss semicolon PL LINEPOINT TREEO pl break S continue ss semicolon PL LINEPOINT TREEO pl continue sd id ss colon PL LINEPOINT TREEl pl label 1 S wait exp ss semicolon PL LINEPOINT TREEl pl wait 2 S goto sd id ss semicolon PL LINEPOINT TREEl pl goto 2 S return exp ss semicolon PL LINEPOINT TREEl pl return 2 S switch exp ss lsect case item l
60. ining enumerations of constants and or integer ranges Types are designated using type expressions A type expression is the name of a type or a list of constants enclosed in braces A colon may partition the list this defines the values before the colon as safe values The constants are strings which do not need quotes in this context unless they contain spaces or integer ranges of the form nn mm where nn and mm are integers The word event may be placed in front of the opening brace to declare an event type An event type has an implied safe value that is the empty string and the given constants are unsafe values type expression id ts 331152025 del t 80 ST 2 ul 02 ss E event el 82 fuse bool lock Named types are defined with the sort set statement but the right hand side type expressions can be used inline as anonymous types Example type declaration sort set id lt type expression gt sort set lt typename gt s0 sl ul u2 3 3 1 Lock Type The lock type is built in to Pushlogic and ranges over any string constant Its safe value is the null string Only the bundle that last set a lock type to a non null value can set it to any other value 3 3 2 Fuse Type The fuse type is built in to Pushlogic and defined as follows sort set bool true false Jj 15 3 3 3 Boolean Type The Boolean type is built in to Pushlogic and defined as follows sort se
61. ist ss rsect PL LINEPOINT TREE2 pl switch 2 4 S disable exp comma list ss semicolon PL LINEPOINT TREEl pl disable 2 S meta pl assoclist ss semicolon PL LINEPOINT TREEl pl meta 2 S live string option exp comma list ss semicolon PL LINEPOINT TREE2 pl live 2 3 38 s_emit exp ss_semicolon PL LINEPOINT TREEl pl emit 2 S never string option exp comma list ss semicolon PL LINEPOINT TREE2 pl never 2 3 S always string option exp comma list ss semicolon PL LINEPOINT TREE2 pl always 2 3 S while ss lpar exp ss rpar pushl statement PL LINEPOINT TREE2 pl while 3 5 S forever pushl statement ss semicolon PL LINEPOINT TREEl pl forever 2 Li S if ss lpar exp ss rpar pushl statement PL LINEPOINT TREE2 pl if 3 5 S if ss lpar exp ss rpar pushl statement s else pushl statement PL LINEPOINT TREE3 pl ife 3 5 7 Ss lsect pushl statement list ss rsect PL LINEPOINT TREEl pl block 2 Li SS lpsect pushl statement list ss rpsect PL LINEPOINT TREEl pl parblock 2 exp ss_colonequals exp ss_semicolon PL LINEPOINT TREE2 pl assign 1 3 exp ss plusequals exp ss semicolon PL LINEPOINT TREE2 pl assign 1 TREE3 pl diadic YYLEAF pl plus 1 3 exp ss minusequals exp ss semicolon
62. iven field must evaluate to a common non bottom value or bottom itself in all possible environments Each rule of a new bundle is checked against the existing participating rules and the bundle is not loaded if any violates this condition PLC2b No race hazards Any program that contains a race of the nature shown in figure 4 1 will not unwind during compilation since the final result depends on the order of interleaving PLC3a Safe Value Constraint A A pair of bundles is incompatible if they disagree on their safe value declarations for any field PLC3b Safe Value Constraint B There must exist at least one setting of the fields such that all executable rules hold and all fields that have safe values defined are set to one of those safe values PLC3c Safe Values Constraint C The safe values of a field must be a subset of the safe values that any expression assigned to that field can safely generate or else the expression must be able to safely generate bottom By safely generate we mean that the expression generates that value when all of its supporting fields are set to their safe values This constraint ensures that when a pushback occurs and an assigned value is set to one of its safe values the assigned expressions can 30 Push In Field s Value An Undo Pushes Out Arrives Undo s Out Figure 4 2 Pushlogic Undo Sequence Failed Update Pusg In Field s Value An Undo Arrives Figure 4 3 Undo Sequence with Race
63. l element xml element list xml att list builder xr 1 results LISTCONS r results H bytecode nothing LISTEND 0 freverse results sd string sd number bytecode LISTCONS TREE2 pl stringtab 1 2 3 sd number bytecode LISTCONS TREE1 pl bytecode 1 2 pushl decls LISTEND 0 nothing module pushl_decls LISTCONS 1 2 pushl statement list nothing LISTEND 0 pushl statement pushl statement list LISTCONS 1 H 2 x A simple xml parser here for reading in compiled bundles and code reflected fragments xml qbody It would be better to handle this xmlq in the lexer x sd id xml qbody sd string xml qbody ss equals xml qbody ss minus xml qbody xml element list ss dltd ss slash sd id ss dgtd LISTEND 0 xml element xml element list LISTCONS 1 xml att list LISTEND 0 2 8 sd id ss equals sd string xml att list LISTCONS TREE2 xml att 1 3 4 H 35 xml_element ss_dltd sd_id xml_att_list ss_dgtd xml_element_list TREE3 xml_element 2 3 5 ss dltd sd id xml att list ss xml singleton TREE3 xml element 2 3 LISTEND 0 sd id TREEl xml chars 1 sd number TREEl xml int 1
64. lement name PK_s gt lt xs complexType gt xs attribute name argls use required gt lt xs complexType gt lt xs element gt lt xs element name PK query lt xs complexType gt xs sequence lt xs choice minOccurs 0 maxOccurs unbounded gt lt xs element PK deqd xs element PK query xs element PK s lt xs element PK_subxr gt lt xs element PK_and gt lt xs choice gt lt xs element minOccurs 0 ref PK_backstop gt lt xs element ref PK_skip gt lt xs sequence gt lt xs complexType gt lt xs element gt lt xs element name PK_and gt lt xs complexType gt xs sequence lt xs choice maxOccurs unbounded gt xs element ref PK deqd xs element ref PK subxr lt xs choice gt lt xs element ref PK_skip gt lt xs sequence gt lt xs complexType gt PK_query gt PK_s gt 18 lt xs element gt lt xs element name PK backstop xs complexType xs element lt xs element name PK_skip gt lt xs complexType gt lt xs element gt lt xs element name PK_deqd gt lt xs complexType gt xs sequence lt xs element minOccurs 0 maxOccurs unbounded ref PK query lt xs element minOccurs 0 ref PK subxr xs element ref PK s xs element ref PK skip lt xs sequence gt lt xs complexType gt lt xs element gt lt xs element name PK subxr type xs NMTOKEN lt xs schema gt Thi
65. lso sports a GTK based GUI if needed and an embedded version that runs on Molly processor cards or on bare PC motherboards without OS A geographical physical modelling system called vworld is currently being developed that enables a number of vir tual interacting pebbles to be visualised on a canvas For checking purposes Pushlogic defines several execution models that succes sively decrease in level of modelling detail All models are suitable for finite state model checking The aim is to enable a more rapid check of a less detailed exe cution model to be verified before proceeding to slower yet more detailed mod elling 1 Message and Component Failure and Network Loss or Delay 2 Message and Component Failure and Network Delay 3 Message and Component Failure 4 Message Failure 5 Component Failure 6 Atomic Reliable Universal Rule Library Expert Script Source Source Source User Interface Creation Bundle Bundle Bundle emacs Phase Source X Library Compilation Phase Compile Time Checker Compiler Canned SCH E oie SCH E XML reflection information Binding Y UPnP and Loading Re Re Re Re Phases Hydration Hydration Hydration Hydration Device Bindings Checker Domain standing rules Jn PT tt Hydrated Hydrated Bundle Bundle Execution Execution Platform Platform Domain of Participation ETC UDP SOAP GENA h Domain Ma
66. ly x fuse Fl forever wait Fl sleep secs 5 Fl false The fuse declaration defines a boolean variable with both values safe and to be set false on bundle load The fuse statement is just syntactic sugar because the line y x fuse F1 is rewritten during initial expansion as if f1 y x During pushback path creation the fuse is chosen as the last option and only marked for push back update if there is no other pushback path available Only the inner most fuse of any nested fuse blocks acts on the enclosed code The reset behaviour is enclosed inside a forever statement equivalent to while 1 and not needed since all push logic sequential sections are enclosed inside an implied forever It resets the fuse five seconds after it has blown If Y y refuses to accept the current value at this time the fuse blows again Other code can be sensitive to this fuse 59 5 11 Pushlogic RPC Currently RPC is not used and all comunication between platforms is imple mented via the shared variable illusion implemented by the tuplecore ETC pro tocol In the future Remote procedure call RPC may be used between Pushlogic bundles or between a Pushlogic bundle and a non pushlogic entity 5 11 1 Foreign RPC SOAP and GENA Pushlogic may make calls directly over the network using XML RPC and in the future SOAP RPC Details to be added Pushlogic can also send and receive GENA events by setting up simple mappi
67. m to str a s 5 2 Abstract syntax tree The abstract syntax tree is defined using the following SML datatype CBG Badger Tuplers Project University of Cambridge Computer Laboratory C 2004 David J Greaves Mostly Written Romsey Dec 2004 1 Oct 05 added parblock and fuse b b db Hb SR db db db Sb x Ob open linepoint datatype pl diop t pl deqd pl dned pl dltd datatype pl type t pl safeunsafe of pl exp t list pl exp t list pl unsafe of pl exp t list pl safe of pl exp t list pl event of pl exp t list pl fielddec of pl exp t list pl type t pl tid of string Id plgram sml v 1 27 2008 07 11 08 15 04 djgll Exp pl dled pl fielddecn of pl exp t list depreciated form zi 44 pl dged pl dgtd fflush stdout pl_logand pl_logor pl_binor pl_binand pl_plus pl pi fusetype pli locktype and pl formal t pl formal of pl exp t pl exp t pl formal nt of pl exp t and pl exp t pl query of pl exp t pl exp t pl exp t pl raw field of pl exp t pl exp t comes in this way from parser x pl string of string pi wtuple of pl exp t list no longer generated x pl tuple of pl exp t list pl id of string pl ellipsis pl backstop pl dollars pl differentiate of pl exp t pl wfield of pl exp t pl diadic of pl diop t pl exp t pl exp t pl catenate of pl exp t string pl num of int pl num range of int x int pl lognot of pl exp t pl apply
68. n be listed on the command line along with an instance name separated by an equals This allows two instances of the same bundle to be loaded Each will put its local fields in its own local tuple named with the instance name for example insl ding plc ins2 din plc 10 5 Console Output Under the debugger it is possible for a Pushlogic program to write strings to the console and to exit with a return code This is done by sending events to certain fields of a local tuple called Platform System Library functions to assist with this are provided Any constant assigned to Platform System sysprint is displayed on the console Any integer assigned to Platform System sysexit causes the platform to return to the OS using the integer as the return value output Platform System sysprint event output Platform System sysexit event 0 255 84 Chapter 11 Other Issues Parasitic Feedback Although Pushlogic rules may not cause a higher level field to change value as a result of a lower field changing in value apart from via undo s there is nothing to stop a Pebble making a cause effect connection be tween a pair of fields in this way Such interactions can lead to oscillation and violate Pushlogic principals Multi media The Pushlogic interpreter is not envisaged as having sufficient throughput to directly manipulate multi media streams Instead multi media streams are started stopped and routed using Pushlogic
69. nager and Checker Execution Phase Execution Platform UDP Broadcast Subnet Figure 1 1 The write compile re hydrate execute toolchain for Pushlogic Pushlogic has been developed for a year or so and its first compiler and run time system are becoming stable We are now implementing the DoP manager that provides real time checking of bundles joining the DoP so that Pushlogic can provide a scripting language for safety critical systems with a dynamic popula tion of sensors actuators and applications We are also adding arrays and remote procedure call clients 1 1 Toolchain Flow Figure 1 1 shows the Pushlogic toolchain Source bundles are compiled with li braries to generate dry object bundles that do not refer to specific pebbles by name A subsequent re hydration stage implements such bindings and a given bundle may join the DOP more than once as illustrated but using different bindings for each instance Several bundles may run on a single execution platform but the behaviour of the system is as far as possible the same as though they were dis tributed over the network For a self contained device using ROM d code such as the Heating Controller presented later part of the re hydration can be performed before canning the code to ROM so that the code is bound to the local pebbles 1Server side RPC requires further study because of the potentially unlimited number of con current activations that must b
70. nd in the supporting parents free fields of its Currently we have implemented our own protocol running over UDP called ETC that im plements the field writes remote registrations for events and code and API reflection but there is little reason not to use the standard protocols 29 A amp amp B if s 1 amp amp A B a OMA ee if s 2 amp amp B if i A amp amp B if S221 amp amp B p if s 3 amp amp A LP Figure 4 1 Example of a Race Hazard POON s s s s assigned expression Vf sup exp leuf lt lev f f exp Fields may be allocated new levels by the system as part of the process of loading a bundle However this is not always successful because a pair of rules in different bundles may have contradictory field level requirements Where the fields are held on different execution platforms a distributed algorithm may be run to establish their levels If this constraint cannot be met the bundle is not loaded The level ordering constraint does not apply to local variables including lock or fuses or compiler generated program counters PLC2 Consistency Constraint A Pushlogic object expression may be deter ministically evaluated in an environment c to produce a string or else the special value bottom L When a rule produces 1 it has no affect on the assigned field All pss To ensure consistency i e to avoid fighting between rules all rules that assign a g
71. ngs between Pushlogic events and GENA events Details to be added 5 11 2 Native RPC Native remote procedure call is provided for communication between Pushlogic bundles on the same or different execution platforms implemented by expan sion to other statements Owing to the dynamic storage restiction limitations of SPL1 a bundle must be re hydrated for each concurrent service operation Block ing RPC is currently being developed the blocking aspect is implemented by expansion to the wait statement Non blocking RPC does not return a result and is denoted with device where the ellipsis is replaced with a list of assignments to mutable fields of that device This is translated to a conjunction of assertions that the appropriate tag fields of the indexed device have the values being passed Blocking RPC is im plemented by the compiler as a combination of non blocking RPC and a wait statement Details to be added here 5 12 OO Structures Some basic syntactic sugar is implemented to enable objects to be defined and instantiated All instantiations are performed at compile time using abstract inter pretation and so must be statically determinable This part of the compiler is currently a bit broken but contains nothing novel 60 5 13 Temporal Logic Assertions Assertions may be included in the Pushlogic source code and checked by the system model checker as well as at compile time or at load time as appropr
72. not to rely on syntax but to use the elaboration rules in the compiler to determine whether a given expression is acceptable in a given con text The rules deny the conjunction of events from separate sources and require that all code reaches closure under repeated symbolic elaboration 85 14 2 The elaboration rules offer a richer language since the syntax directed form cannot easily encompass concepts of an differentiator enclosed in an integrator 4 5 1 Syntax directed guide to level and event expressions The following rules would be broadly sufficient to distinguish level expressions from event expressions but they are intended as a guide to programmers and are not a definition A level expression is essentially an expression with no leaf variables of type event and which does not contain the differentiation operator It maintains its value unless any of the supporting variables changes their current value their level in hardware terms An event expression is a function of one or more variables of type event or which contain the differentiation operator Not all operators support event ar guments those that do are conjunction disjunction and conditional expression query colon construct negation of events is forbidden Disjunction of event expressions logical OR is always allowed but conjunction requires that both ar guments stem from a single external event delivered to the current bundle The basis of this is that sim
73. ntee style automated reason ing Real time Model Checking is one of our main challenges being explored 8 3 Federation of Pushlogic DoPs Pushlogic rules hold within a domain of participation DoP The DoP may cover multiple execution platforms but all rules are shared in terms of consistency checking Variations on this model are required in practice to provide localised behaviour and assur ances to dynamic allow merging and dividing of domains and to provide federation of domains where knowledge about peer domains is available in summary form only 77 Chapter 9 Pebbles and Pebble Formal Model Pebbles themselves are self contained hardware or software objects that fulfill a certain task Examples are a numeric entry keypad an electronic piggybank or a speech recognition engine Our vision is that all such devices shall in the future share a common middleware and reflection API A pebble that is compatible with the Pushhlogic Tuplecore system is defined for mally here The XML schema for such a Pebble follows exactly the same struc ture An uninstantiated pebble is a quad of a type name pebble_dataplane and peb ble behaviour A type name is a string that is unique name for an uninstantiated pebble It is sensible to use use URI s as type names since these can ensure uniqueness but other mechanisms can also be used A pebble dataplane is a set of field name field domain field type field value
74. odel provided there are few of these constructs but complexity will eventually mount up in meta constraints over the fresh variables that model the possible firing orders Here is a bundle that is incompatible with the ButtonLock both cannot be loaded into the same DoP To explain this first we must mention that we have not fully im plemented the re hydration stage yet and so hardcoded identifiers such as the IP address of the other bundle s platform are currently hardcoded in the source files The button variable was originally free to change at any time but becomes con strained by the second bundle to only change while the unlocked variable holds The system cannot be unlocked without the button being pressed and hence the live assertion in the Button listing fails This will in future be spotted by the DoP manager but currently can only be spotted by the compiler checking against pre compiled bundles that are to hand def bundle B2 pebble r tup 128 232 1 45 v input d q bool r keys button r locks unlocked amp amp d q 5 14 Compiler Operation It is helpful to briefly present the internal operation of the compiler The internal flow of the compiler is shown in Figure 5 2 5 14 1 Conversion to I Code The input is parsed and converted to imperative intermediate code using conven tional compiler techniques Function calls are expanded in line For each sequence 62 Source Code Parser Exp
75. of pl exp t pl exp t list pl par of pl exp t pl exp t The following do does not occur in yacc parse tree x pl raw fieldl of pl exp t list pl fillerl x Used only to supress the unused cases warning in my other match traps zi Old form compiled bytecode files zi datatype pl comp t pl stringtab of string int pli bytecode of int H datatype xml_t xml element of string x xml att t list xml t list xml meta of string xml int of int xml chars of string and xml att t xml att of string string i A transitioner should be one of entry body exit x type pl transitioner t string datatype dv t dv output dv input dv inout dv local dv fuse dv lock dv tuple dv other datatype pl case item t pl case item of pl exp t list pl cmd t pl case default of pl cmd t and pl cmd t pl if of pl exp t pl cmd t pl while of pl exp t pl cmd t pl forever of pl cmd t pl ife of pl exp t pl cmd t pl cmd t pl switch of pl exp t x pl case item t list pl assign of pl exp t x pl exp t pl pragma of string pl exp t pl block of pl cmd t list pl parblock of pl cmd t list pl with of pl exp t x pl cmd t pl fused of pl cmd t pl exp t pl wait of pl exp t pl goto of string pl label of string pl break pl continue pl emit of pl exp t pl return of pl exp t pl assert sl of string bool pl exp t pl never of string option pl exp t list pl always of string option
76. oint from any string L does not need to be explicitly written in the Pushlogic source level A full list of operators should be given here Note that string cat uses dot and is XOT A FOGT operator is provided that performs a comparison in the style of greater than but with the assumption that a pair of integers in a adjacent quadrants of the number space have not lapped each other Example needed here 4 4 Fields and their Declaration Our current main Pushlogic implementation is part of a distributed tuple space platform and hence variables are called fields Most fields are either events or range over the constant string integer values defined above Apart from strings integers and events the tuple space platform supports some other types including level primary key credit URI and so on Their definition is beyond the scope of this document and so only mentioned in passing A tuple is a collection of fields each named with a tag string A field may contain a nested tuple Every tuple has a field called level 1 e the tag string for that field is level It contains a negative integer lev v Z7 All fields and tuples are part of a global shared address space and in principal can be accessed from any bundle However the concepts of domain device pebble and bundle each impose overlays of name aliasing and access control on the global space Certain tuples are associated with the current DoP certain wi
77. ome level in the system or else we must essentially have a set of locks indexed by requester name that implements a variant Dijkstra s solution Pushlogic allows a field to be declared as a Lock whose safe value is the null string More than one bundle may store a non safe value in a lock field relaxing the normal rule but such a store is only successful if the previous value was the null string In a network race the second client that attempts to store a non null value will experience a pushback 6 4 2 Make break Issues Where an event triggers the change of two or more fields sometimes the order in which they are changed is critical For instance electrical changeover switches come in make before break and break before make varieties Since Pushlogic is a relatively high level language built in support for make break ordering should perhaps be provided for the common cases rather than forcing the programmer to implement his own sequencers However this is for 72 future study What is implemented is checking over various message delivery skew and loss scenarios 1 4 6 5 Low level Parallel Composition of Tuples Both the pebble statement in Pushlogic and the binding performed at re hydration implement mappings between identifiers in a Pushlogic program and other parts of the Tuplespace typically tuples in Pebbles Sometimes it is helpful for there to be more than one concurrent binding in place For instance
78. one bundle definition that contains all of the rules as well as further declarations Comments are defined with the BCPL style double slash 5 4 Bundle Declaration def bundle mybundlename contents go here A bundle declaration uses the keyword sequence def bundle The bundle content is a list of declarations and statements The bundle name should com monly be the same as the program file name on the storage media The statements in a bundle are all started in parallel when the compiled object bundle is loaded A statement may be a sequential block thereby providing the normal imperative programming paradigm 46 Each item within a bundle definitions is either a declaration a first order or tem poral logic assertion or an executable sequence of imperative code Executable sequences are composed in parallel Each sequence may be considered to be en closed in an infinite while loop that has its own thread that executes the rule as fast as possible but with all such threads of the bundle performing their next assignments in synchronism Sequential composition of behavioural statements is introduced with the block construct denoted with C like open and close braces A further level of parallelism is possible inside a sequential block because parallel assignment is supported e g a b el e2 Bundles may also be declared using def pebble def world and def plant The pebble declaration allows soft
79. one write command There is also a pushdown operation for tuplecore use but that is not currently used 81 10 1 Registration A platform must announce its presence and register with one or more domain manager s We have had various registration technologies including O2S Atif is currently implementing UPnP and RDF registration Device API reflection is currently achieved through the code reflection interface 10 2 Code reflection A platform exports the source code of its running bundles including the assertions about the operation of the enclosing domain that its bundles have made This is called code reflection Code reflection is achieved using an HTTP GET and the code is encoded in XML 10 3 Web Interface Many platforms implement a web interface that allows web based viewing of in ternal state and a certain amount of commanding The web server provides XML and also a canned CSS style sheet for easy viewing 10 4 Pusher Command Line and GUI Tool The interactive interpreter for pushlogic on workstations is called pusher Pusher can be run standalone on a workstation with a number of bundles loaded from the command line Figure 10 1 shows a bundle called Lanterns under the GUI The output outside lantern is a label and cannot be changed directly with the GUI It is updated when the value of this variable changes The input mains supply has a menu from which the user can select on or off Th
80. or nil LISTEND 0 value list 1 value list value LISTCONS 1 value value_list LISTCONS 1 H LISTEND 0 2 exp expl 8 1 expl exp2 ss query expl ss colon expl TREE3 pl query 1 3 5 exp2 1 exp2 exp3 1 exp3 ss rarrow2 exp3 TREE3 pl diadic YYLEAF pl implies 1 exp3 exp4 1 exp3 ss rarrow2 exp4 TREE2 pl implies 1 3 exp4 exp5 8 1 exp4 ss logor exp5 TREE3 pl diadic YYLEAF pl logor 1 instead of for integer ranges An 3 3 41 exp4 ss_disj exp5 TREE3 pl diadic YYLEAF pl_logor 1 3 exp5 exp6 1 exp5 ss logand exp6 TREE3 pl diadic YYLEAF pl logand 1 3 exp5 ss caret exp6 TREE3 pl diadic YYLEAF pl xor 1 3 exp5 ss conj exp6 TREE3 pl diadic YYLEAF pl logand 1 3 exp exp7 1 exp7 ss_deqd exp7 TREE3 pl diadic YYLEAF pl deqd 1 3 exp7 ss dned exp7 TREE3 pl diadic YYLEAF pl dned 1 3 exp7 ss dltd exp7 TREE3 pl diadic YYLEAF pl dltd 1 3 exp7 ss dled exp7 TREE3 pl diadic YYLEAF pl dled 1 3 exp7 ss dgtd exp7 TREE3 pl diadic YYLEAF pl dgtd 1 3
81. orms e provide compute resources for soft pebbles e provide model checking over all rules in the domain to ensure all properties are satisfied and e support removal of devices bundles and pebbles when no longed wanted The Domain Manager provides a few standard pebbles used by Pushlogic in read only mode that provide domain status information Bundles run inside a domain of participation DoP Dynmaic storage allocation only occurs when new bundles of rules are loaded into a running DoP Bundles arrive either when a new pebble that requires control arrives or when a new appli cation is started expressed in Pushlogic Before a bundle can be loaded the union of the rules in the new bundle is formed against those already in the domain If any of the rules are inconsistent or any of the temporal logic rules existing or new will not hold under the combined mechanism the bundle cannot be loaded 76 8 1 Using the compiler to check domains It is planned that a number of compiled bundles can be read in during a com pilation and the bundles being compiled are checked against them Indeed no source level bundles are provided the compiler will act as a static checker for a collection of object bundles This has been implemented but no examples written up 8 2 Incremental and Real time Model Checking We wish to design an object bundle file format that is as amenable as possible to rapid incremental model checking or assume guara
82. ot also unloaded at the same time A bundle might require parts of it to be loaded onto different execution plat forms for efficiency but the underlying tuplecore implementation means this is not strictly necessary since all points of the tuplespace are nominally accessible from anywhere Operational model 1 5 Re Hydration A bundle of rules may be re hydrated before being offered to the domain This means expanding various hierarchic macros in the rules to produce flat Pushlogic Object code The number of rules in a bundle may be increased or decreased during re hydration For instance a complete bundle of standard rules may be copied out from a store where they are held in a canned form Macro generation is needed because Simple Pushlogic SPL1 has no bindings pointers objects or dynamic storage allocation The macro generation ameliorates this by generating rules with static fields Pushlogic rules may directly refer to fields with absolute path names as part of a global tuple space or to fields local to the current execution platform gener ally the current device or to the current domain of participation In a general situation this is not sufficient Rules need to refer to locally bound devices such as front door bell Re hydration provides such binding It also provides guar anteed uniqueness for certain field names needed in applications that require the equivalent of local variables Researc
83. parts of this list The range of values is partitioned into safe and unsafe values The the list of safe values is definitive whereas code should operate correctly and all assertions pass if further unsafe strings or integers occur during run time This supports dynamic system extensibility The elipsis construct is allowed in list of unsafe value at the the pushlogic source level but serves only to alter behaviour with respect to compile time warnings One of the safe values the first listed in any list is known as the nominal starting value for that field and can be used as such in offline checks that involve reachable state analysis When a bundle or pebble is introduced to a DoP if the nominal starting value of any of the the newly created fields associated with the new bundle or pebble is inconsistent with extant domain values fields may be set to any value that makes the rules consistent but with priority being given first to nominal starting values then to other safe values then to listed unsafe values If insertion of a new bundle or pebble into a DoP would immediately cause a pushback inside the domain this should perhaps be flagged at a meta level to the operative attempting the insertion 25 4 5 Level and Event Expressions Expressions are either level or event expressions It is possible to define the dis tinction in a syntax directed way as given shortly However the current and pre ferred implementation is
84. pebbles to be defined fully using Pushlogic Pebbles have slightly different rules over binding of shared fields from bundles details to follow 5 5 Constant Values Constants may take the same forms as those define in 3 1 for object level except that bottom is not allowed at source level 5 6 Identifiers Identifiers appear alone or as part of an heirarchic field name Identifiers appearing alone must be either a member of one or more field range enumerations the last component of an heirarchic field name or the reserved iden tifiers true or false Where the last component of an heirarchic field name is shared over more than one field or is also a constant value from a field range enumeration the identifier cannot be used alone it must be placed in double quotes to imply the constant value or to refer to a field must be disambiguated by providing further trailing portions of the heirarchic field name or using by using a with statement The alone use of identifiers is not currently working in the compiler always 5 7 Field Declarations Variables are known as fields Field declarations define the heirarchic name of the field its name and then partially enumerate the ranges of safe values and unsafe values delimited with colons The safe and unsafe enumerations for must be disjoint for any one field 47 If the colon between the safe and unsafe values is ommitted all listed values are unsafe
85. quads where the field names are disjoint A field name is a list of strings The last string is the final field name and the and others are tuple names By convention field names are in lower cases and tuple names are capitalised first letter is a capital letter Field names that are only different in their final field name are said to be part of the same tuple Us ing Pushlogic field names are written with a hash sign between each string for instance Pebbles Lamp status A field domain is a disjoint union of safe and unsafe lists Each member of the safe and unsafe list is a field domain specifier A field domain specifier is a string constant or an integer an integer range or an ellipsis Please see 85 7 for the concrete syntax for field declarations used in Pushlogic A field type is one of the following values fluent event read only lock money Most pebbles only use the fluent type for all fields A fluent is a conventional variable that retains its most recently written value and returns this value when read 78 A field value is a constant string that conforms to the field domain It is set to the first item on the safe list when the pebble is first created or reset A field value may be interpreted to have integer or real semantics in some contexts but it is primarily a string There is no NULL string but the string of zero length is allowed When interpreted as a boolean all values are true except for fals
86. reference but have special meaning at the start of a field name Dot may also be used but is intended for access to components within the OO parts of the language A field name starting with a dollars sign is a local field name These need not be used since the compiler provides the special Local keyword that defines aliases so that local variables may be stored in the bundle s private area In an implementation the dollars symbol is mapped during re hydration to a fresh tuple stored on the local execution platform whose primary key is the bundle instance identifier When the name starts with a hash it is interpreted with respect to the field prefix given in a textually surrounding with statement If there is no surrounding with statement then the reference is to the namespace of the local device This is also the default namespace when no leading character is given and the field reference starts with a tuple name A field name starting with a slash refers to fields provided and stored within the current DoP Field names may also start with a URI or a symbolic name that is converted to a URI during re hydration A more detailed description of heirarchic names is outside the definition of Pushlogic and are defined in the Tuplecore document and web pages The pebble alias statment establishes a pointer to part of the namespace It is frequently used to provide a Pushlogic bundle with access to pebbles instantiated 4
87. rgs left right and pushback info No postfix attributes CODE PK query 14 Conditional expression operator Four stack args guard true exp false exp pushback info No postfix args CODE PK degd 15 Equality comparison operator Three stack args left right and pushback info No postfix attributes CODE PK dgtd 16 Greater than comparison operator Three stack args left right and pushback info No postfix attributes CODE PK dged 17 Greater than or equals comparison operator Three stack args left right and pushback info No postfix attributes CODE PK plus 20 Addition operator Three stack args left right and pushback info No postfix attributes CODE PK minus 21 Subtraction operator Three stack args left right and pushback info No postfix attributes CODE PK tup 22 Reference to a tuple in the current domain of participation Sometimes currently used instead of localroot No stack args One postfix attribute the tuple name CONSTANT VALUES CODE PK s 1 Defines a string constant No stack args One postfix attribute the string itself 20 CODE PK_backstop 19 A constant value which when assigned does not change the current value No stack args No postfix args CODE PK_int 25 No stack args In bytecode a representation of integers in base 256 In XML integer elements appear directly CODE PK_nint 26 No stack args In bytecode a representation of integers in ba
88. s an alias for while 1 5 10 12 Procedure Call Statement A procedure call statement has no keyword A call consists of a function name followed by its arguments in parenthesis Procedure calls are expanded at compile time and hence must have a compile time determined upper bound on recursion depth 57 5 10 13 Return Statement The return statement is for use in functions only An example def fun add a b c if a red return b return c d 5 10 14 Wait Statement while 1 wait expr The wait statement cause the current thread to wait until a condition holds There are no threads in Pushlogic object code and so the wait statement is imple mented by splitting the source code into separate basic blocks that are guarded by values of an automatically defined enumeration that chains control from one block to the next The enumeration variable acts rather like a program counter At runtime it is stored in the field local pcnnn where nnn is an integer that is unique to a bundle To avoid inter bundle name space clashes all fields in starting with local are renumbered to be disjoint at bundle load time The same mech anism is used to create a hidden variable to store the old value of a field by the differentiation operator denoted with the uparrow SOME REPETITION HERE The wait statement blocks the current thread until the condition holds If the thread loops around and enters th
89. s schema is partial since it does not currently list all of the diadic operators The PK_skip statement is shown instead of the pushback info in this version 4 0 Virtual Machine The bytecode is defined in this table Pushlogic Byte Code Descriptions DRAFT For the bytecode representation self describing args preceed the bytecode and fixed field args follow the byte code For the XML representation self describing args are included as sub elements of the element and the fixed field args are put as attributes OPERATORS CODE PK and 2 Logical and function Three stack args left right and pushback info No postfix attributes CODE PK or 3 Logical or function Three stack args left right and pushback info No postfix attributes CODE PK not 4 Logical not function One stack arg No postfix attributes CODE PK inv 5 Bitwise complement One stack arg No postfix attributes CODE PK xor 6 Logical xor function Three stack args left right and pushback info No postfix attributes CODE PK divide 32 Division operator 19 Three stack args left right and pushback info No postfix attributes CODE PK_mod 33 Modulus operator Three stack args left right and pushback info No postfix attributes CODE PK fqgt 34 Four quadrant greater than operator Three stack args left right and pushback info No postfix attributes CODE PK multiply 35 Multiplication operator Three stack a
90. se In XML integer elements appear directly CODE PK_ellipsis 28 A constant value which denotes other possible values in a domain declaration No stack args No postfix args CODE PK_range 29 Declares a subrange of the integers Two stack args from and to inclusively No postfix args TOP LEVEL ITEMS CODE PK_rule 7 Defines an executable rule Six stack args are left hand side tuple left hand field right hand side pushback spare and spare In XML form the left hand side tuple and field are combined and use a single element One postfix attribute nominally called timeout but currently unused CODE PK_subxw 8 Define a subexpression One stack arg any expression One postfix attribute the subx number CODE PK_subxr 9 Read a subx defined by subxw Zero stack args One postfix attribute the subx number CODE PK domain 30 Declares the range of values for a field Stack args the safe values followed by the unsafe values Three postfix args type safe values unsafe value CODE PK safetylive 24 not used now An Oldform CODE PK sl 40 Safety live rule definition Three stack args guard true false and message No postfix attributes The middle value is true for a safety rule and false for a live rule The message should be reported if the rule fails Fairness constraints are to be added CODE PK fieldl 41 not used anymore 21 FIELD AND TUPLE ACCESS CODE PK_localroot 13 Explici
91. sed inside any conditional statement such as an 56 if or case statement in which case it is as though all of its internal activity is guarded by that condition the condition is simply folded inside every construct to the point where a conditional is allowed The stategraph does not reset to its starting state when this guard does not hold A stategraph with a state called disable may be disabled from elsewhere in the same bundle using the disable statement Please see 85 10 10 The stategraph general form is sufficient to encompass the SysML state machines 5 10 10 Disable Statement The disable statement is used for a remote disable of a stategraph Syntax if g disable stategraph namel stategraph name2 The disable statement must be conditional otherwise the stategraph would never leave its disable state and the disable guard g may either be an event or level expression When the disable guard is a level expression it takes precedence over any transitions in the stategraph that lead from the disable state if g disable stategraph namel stategraph name2 5 10 11 While For Break Continue Statements The while continue break statement as found in the C language is sup ported The for continue break statement as found in the C language is sup ported The do while continue break statement as found in the C language is not yet implemented The forever statement i
92. t bool true false Jj The sort bool is already defined by the system and contains the reserved con stants false and true both as unsafe values It is an error to define any field to range over the reserved constants false or true unless the field ranges over exactly these two fields They may be safe or unsafe Examples sort set d0 bool OK making use of predefined sort sort set dl true false OK true is safe sort set d2 true false OK both unsafe same as boolean sort set d3 false 0 9 Illegal sort set d3 false true red brown j Illegal 16 Chapter 4 Pushlogic Object Level VM Execution Pushlogic originally generated its own native object level bytecode This was considered the reference standard for code reflection Anything that generated this form of code could particpate in the system Now 2008 the Pushlogic compiler also generates net IL code The code can be checked whether conformant to one or more checkablity profiles and the do main manager will reject bundles that are outside its supported set of checkability profiles 4 1 Code Reflection Schema Pushlogic native object level is considered the primary form of represenation It exists in bytecode and XML forms The XML schema for Pushlogic code reflection is as follows A separate schema is used for data reflection via the tuplecore todo where is i
93. t listed lt xml version 1 0 encoding UTF 8 lt xs schema xmlns xs http www w3 org 2001 XMLSchema elementFormDefault qualified gt lt xs element name bundle gt lt xs complexType gt xs sequence lt xs element maxOccurs unbounded ref PK subxw lt xs element maxOccurs unbounded ref PK domain xs element maxOccurs unbounded ref PK rule lt xs sequence gt lt xs complexType gt lt xs element gt lt xs element name PK_subxw gt lt xs complexType mixed true gt xs sequence lt xs element minOccurs 0 maxOccurs unbounded ref PK fieldr lt xs sequence gt lt xs attribute name no use required type xs integer gt lt xs complexType gt lt xs element gt lt xs element name PK_fieldr gt lt xs complexType gt lt xs choice gt lt xs element ref PK_fielda gt lt xs element ref PK_tup gt lt xs choice gt 17 xs attribute name argls use required type xs NCName gt xs complexType lt xs element gt lt xs element name PK_domain gt lt xs complexType gt xs sequence lt xs element minOccurs 0 maxOccurs unbounded ref PK s lt xs element minOccurs 0 ref PK ellipsis xs element ref PK fieldd xs sequence lt xs attribute name mode use required type xs NCName xs attribute safecount use required type xs integer gt xs attribute spare use required type xs NCName xs attribute unsa
94. t name for the local root tuple sometimes currently omitted by implication No stack args No postfix args CODE PK_uri 27 Reference to a tuple on another execution platform No stack args One postfix attribute the uri CODE PK_fielda 23 A field reference where the field contains a tuple One stack arg a tuple One postfix arg the field name CODE PK_fieldw 10 A field reference for writing One stack arg a tuple One postfix arg the field name to be written CODE PK_fieldr 18 A field reference for reading One stack arg a tuple One postfix arg the field name to be read CODE PK_fieldlk 39 A field declaration where the field will be a lock One stack arg a tuple that will contain the field One postfix arg the field name CODE PK_fieldd 36 A field declaration One stack arg a tuple that will contain the field One postfix arg the field name MISCELLANEOUS CODE PK_eventr 42 event read pushlogic interepreter internal use only Does not appear in bytecode currently inferred by bcload CODE PK_pbind 37 Pushback info 2 currently being changed sligthtly CODE PK pbval 38 Pushback info 22 currently being changed sligthtly CODE PK meta 11 Not used CODE PK skip 12 A nop No stack args No postfix args CODE PK eob 31 End of bundle marker not used in XML form No stack args No postfix args EOF The XML schema essentially follows the bytecode in that a ver
95. taplane 9 0 2 Bundle Metainfo Reflection via Pebble Dataplane 10 Execution Platforms 10 1 Registration 10 2 Code reflection 10 3 Web Interface 10 4 Pusher Command Line and GUI Tool 10 4 1 Pusher Command Line Arguments 10 5 Console Output 11 Other Issues 78 79 80 81 82 82 82 82 83 84 85 Chapter 1 Introduction In software terms a script is a collection of commands to be performed in a particular order under various conditions Imperative programming languages such as assembly language Java and the unix shell language are frequently used for scripting These languages are used to control a collection of devices or to otherwise automate a process They are unrestricted in expressibility and hence reasoning about their behaviour or their interaction with other such scripts is hard When a script phrased in a decidable language controls and reacts to objects con taining undecideable code or exhibiting unpredicatable behaviour the system becomes undecidable as a whole Nonetheless it is our belief that there are sig nificant benefits from using decidable code at the highest levels the level of ap plication scripting Model checkers are good at exploring system behaviour over all possible behaviours of the undecidable subsystems In our approach complex autonomous or undecidable behaviour is partitioned and placed in pebbles that interact using a constr
96. terministic presence guard for each unloadable bundle by the domain manager PLC7 No oscillations constraint Oscillation is created by inverting loops Any bundle that contains an internal oscillating loop cannot be elaborated by the com piler and causes a compile time error When bundles are brought together with each other or world models any oscillators then formed are detected by the do main manager and the union is not allowed For example the following two lines are inconsistent since they form an oscillator If the lines are in the same bundle a compile time unwind fail error is flagged If they are in different bundles but the variables are bound to form a distributed inverting loop then the oscillation error is flagged by the domain manager a b b la Many device control loops are oscillators such as those used in thermostats In order to implement these the loop must be broken using a time delay at some point to regulate the maximum freguency of oscillation For example with Timer Countdown if atimer 0 tatimer 1000 Delay for one second b_delayed b a b delayeg b rs la Resynchronisation Constraint A liveness predicate expresses that two supposedly coupled systems will eventually become re synchronised after network distruption has finished 4 9 Temporal Logic Assertions A bundle may contain a number of safety or liveness assertions These take ex pressions as arguments and
97. tes to fields held on the same execution platform as the Pushlogic that arise owing to a single event are batched and made at once atomically Further changes arising from a batch of gated updates are collected and deferred to the next batch An event nominally holds for one gated cycle All event fields are re set to the null string after the cycle where they were processed 4 6 1 Nominal Meaning of a Rule A Pushlogic rule is to be thought of as holding at all times except when it is assigning L at which times the assigned field retains its current value or is con trolled by another rule Push Logic is designed such that each rule may also be interpreted as an assertion about the current state of the assigned field and the con junction of all such assertions should hold at all times However because fields may be held on physically separate devices and Push Logic interpreters inter change network messages when fields need to be changed this conjunction will not globally hold for brief periods while network messages are in flight or during network disconnect 4 6 2 Event and Level Constraints The occurance of event expresions in executable rules is restricted by the follow ing schema The executable rule must be factorisable into one of three forms where ee denotes an event expression le denotes a level expression lv denotes a level variable and ev denotes an event variable The four forms are lv le le 1s 27 ev
98. th the current device 24 or execution platform and certain exist only for private local access by the current bundle Like a bundle a pebble also possesses a set of associated local fields but these are not private indeed they are used as shared variables for communication with the Pebble As a coding convention users of Pushlogic are invited to use first letter capitali sation for then names of fields that contain tuples and lower case for fields that are variables Fields that are local to the current bundle are declared with the keyword local Fields that are shared and provide input or output to the current bundle are de clared with the keywords input inout or output Actually at object level the keywords are replaced with Pushlogic bytecodes The built in types such as Lock bool or fuse can be used at source level as a short hand to declare local fields For example the following two lines show equivalent ways of defining booleans local varl var2 bool bool var3 var4 The definition of fields and tuples is identical at source level and object level and is unchanged by the compiler When a field is declared a range of values for it may also be declared If the range is to be used frequently it can be named and represented as a type and then refered to by its name The range is denotation of a list of constant strings but integer subranges can be used to specifiy
99. the expressions have the form defined in 84 3 Object level safety and liveness assertions are checked by the Domain Manager at bundle load time They are retained by the Domain Manager for further checking against newly arriving bundles Monotonicity constraints imply they cannot be violated by bundle or pebble departure 33 Chapter 5 Pushlogic Source Language NB There is a user manual for the source compiler in html on the website This chapter discusses the source language per se rather than how to compile it Although rules are frequently a useful way to express desired behaviour many ap plications are most easily coded in an imperative programming style Rather than expecting the user to manually convert his notions of application behaviour into Pushlogic object rules a compiler for imperative style expression of applications is used We note that imperative programs deal essentially with sequential changes of state whereas logical predicates over application programs deal in terms of the visible accumulated results of these changes Pushlogic Source is a block structured imperative like programming language but with no dynamic storage allocation and currently no arrays It is less funda mental to our approach than the object form because a variety of source forms could be envisaged that would generate compatible object for various niche ap plications The Pushlogic constraints on a bundle are implemented at bundle lo
100. tion a tightly coupled field is any field held on the same execution platform and these are readily determined because their path name starts with the local root The int diff constraint provides that an infinite while loop wrapped around a par allel statement that contains no internal waits is not sensitive to the additional loops made by the thread PLC 6a Montonicity constraint All rules must meet the other constraints with any amout of extension to the range of unsafe values in any field The constraints on allowable Pushlogic programs union of unbundled rule bun dles have just been presented These constraints can be checked without full possession of the Pushlogic object code This could be very useful in large sys tems or where IP or policy needs to be protected A summary form for a bundle may be defined that lists for each assign field the level constraints and the pos sibly assigned values Where the Pushlogic Timer or other common resource is frequently depended on then the summary can helpfully mention this explicitly For instance a set of different bundles might control a common field at different times of day and these would appear incompatible if time were ignored but by including it in the summary the bundles become compatible PLC6b Montonicity constraint Any bundle whose assertion guarantees rest 32 on the presence of other bundles that might become unloaded is not allowed This is checked using a non de
101. tk to exercise the GUI It creates a gtk label for output and local variables which are updated with an upcall from the tuple substrate For inputs it creates either a gtk scale if the domain is an integer range or a gtk combo box i e a menu for an enumerated type Th pusher interpreter may also pretend to be an execution platform pebble mean ing that it might beacon some metainfo so that a domain manager gives it some bundles to run 10 4 1 Pusher Command Line Arguments Command line arguments are compiled bytecode bundles or options The nogui command line option disables the GUI and directs all output to the console The cycles nn command line option makes the platform exit to the OS after so many seconds The tupdump command line option prints the internal tuplespace to the console every few seconds Bundles should have suffix p1c and this is added if no dot is present in the filename Alternatively bundles should have suffix plox Bundles with a x suffix are XML coded bundles as reflected from execution platforms NB the compiler pushcomp generates four object files from each compilation two of which are loadable by pusher and the remainders are for can ning to device ROMs pushlogic bytecode or net bytecode Bundles are loaded from the current directory or any directory listed on a colon 83 separated list of directories stored in the PLPATH environment variable Bundles ca
102. to set up the connection parameters although not to copy the data itself In this scenario the embedded application is having a proactive effect on other Pebbles in the local environment for instance it is routing audio and video to them We use the term feature interaction to describe the general situation where independent application scripts try to perform disagreeing operations on a Pebble at the same time In the DVD example feature interaction would arise when two DVD players try to route video to one display at once Using the Pushlogic approach all application scripts within an environment of participating devices must either be implemented in Pushlogic or else summarised in it The various routes to using Pushlogic are illustrated in figure 1 1 A high level language such as Pushlogic Source is compiled by the compiler to generate the Pushlogic object code This is then canned in ROM for direct interpretation in the embedded target or further compiled to native code for a micro controller The latter approach may serve to use less RAM In all routes a Pushlogic form of each application is made available for checking in advance of the application being allowed to join the environment of participation We use the term code reflection for the concept of application software being examinable in some for or another 1 2 Bundles Pushlogic programs consist of bundles of rules A bundle must be checked be fore it is
103. ultaneous delivery of external events is not meaningful 4 5 2 Assertions on Level and Event Expressions The always assertion asserts that a condition must always hold and its argu ment must be a level expression The never and live assertions may apply to either type of expression Further temporal logic operators such as until and w until and gen eral CTL expressions are not currently supported but will have the requirements on their arguments that would arise from decomposition into safety and liveness form 26 4 6 Executable Rules Each executable rule is an assignment of the form T exp pbind where f is a field a scalar variable name in a global name space and exp is a Pushlogic object expression and pbind is compensation information that asists in reversing the operation of the rule This information also identifies certain of the expression support i e certain of the free variables occuring in exp as the sensitive parents of the rule All pushlogic rules at the object level are composed in parallel and execute si multaneously D1 Rule Execution The reference execution model for an executable Push logic rule is that all subexpressions occurring in the expression are re evaluated whenever there are changes to any of their support Likewise changes to the result of the top expression become scheduled as updates to the assigned field Updates are gated by which we mean that all upda
104. urrent stategraph and an optional statement to be executed when taking the transition In situations where multiple guard expressions currently hold the first holding transition is taken The guard expressions range over the inputs to the stategraph which are the vari ables and events in the current textual scope and the exit labels of child state graphs When a child stategraph becomes active it will start in the starting state name is given as an argument to the instantiation or the first state of no starting name is given A child stategraph becomes inactive when its parent transitions even if the tran sition is to the current state in which case the child stategraph becomes inactive and active again and so transitions to the appropriate entry state A child stategraph can cause its parent to transition when the child transitions to an exit state There may be any number including zero of exit states in a child stategraph but never any in a top level stategraph The parent must define one or more transitions to be taken for all possible exit transitions of its children An exit state is either called eut or exit id where wd is an exit tag identifier Exit tags used in the children must all be matched by transitions in the parent or else the parent must transition itself under the remaining exit conditions of the child or else the parent must provide an untagged exit that is used by default A stategraph may be wholly enclo
105. ut recursion is not allowed The stategraph general form is stategraph graph name state statename0 subgraph name subgraph entry state entry Statement exit statement body statement Statement eee implied body statements Statement cl gt statenamel statement C2 gt statename2 statement C3 gt exit good exit good gt statename3 statement exit bad gt statename4 statement endstate state statename2 55 endstate state disable A special state that can be forced remotely A state may contain tagged tatements each of which may be a basic block if re quired They are distinguished using three tag words The entry statement is run on entry to the state and the exit statement is run on exit The body statement is run while in the state A body statement must contain idempotent code so that there is no concept of the number of times it is run while in the state Statements with no tag are treated as body tagged statements Multiple occurrences of state ments with the same tag are allowed and these are evaluated as though executed in the textual order they occur or else in parallel current implementation is serial but this will be change to parallel so watch out A state contains transition definitions that define the successor states Each tran sition consists of a boolean guard expression the name of one of the states in the c
106. wait of bc t T 6 OR be ves mnt I eof I skip I safetylive of bool zx bc t x safe is true x Runtime program counters range only over the entry point to a thread and the points immediately following an I wait The I code is embedded in a BDD package by generating binary encodings of every variable field constant and operator This then enables an equivalence checker to be used to compare any pair of expressions or check that a predicate is a tautology 5 14 2 Repeated Elaboration from each Entry Point until Clo sure An entry point is defined as any entry point to a section of I code or the location immediately after any wait instruction Parallel symbolic evaluation is then con ducted until closure or failure if more than 100 iterations is needed This consists of starting in a null environment and evaluating from each entry point to collect symbolically the assigns to every variable including program counters up until a wait statement or the thread loops back to its initial entry point Function calls are expanded in line 64 Elaboration of assignment While more than one assign is made to a variable by different threads such as v el v e2 the assignments are combined in pairs using the following rule v el ted el check el e2 V el Ve2 2T his gives a single expression for every assigned variable If the check fails the compilation fails because the operations are incompatible Elaboration o
107. y simple tree walker is all that is needed to convert XML form to bytecode The current push logic interpreter indeed converts it in this way Pushlogic has three forms of representation source canned object and re hydrated object In this section we give the semantics of re hydrated object which is re garded as the primary form of Push Logic It is actually a bytecode suitable for automated checking distribution and loading into an execution platform byte code interpreter A Pushlogic program at the object level is a set of rules known as a bundle Pushlogic programs are aggregated into a domain of participation by disregarding bundle boundaries and forming the union set of rules but a bundle may not be admitted if automated formal tests fail for any rule within it These tests are given below Each one is called a constraint A race can arise if an attempt is made to load a pair of incompatible bundles at once the system will accept only the rules from the first bundle Pushlogic object rules have three forms executable liveness and safety The source compiler can convert more complex temporal constraints into a conjunction of live and safety checks for the object form to handle Liveness and safety rules are assertions to be checked by a model checker invoked by the loader The loader also has certain built in constraints described below that require model checking The model checker can be run as a network service or

PDF Version

Contents

Download Pdf Manuals

Related Search

Related Contents