Home

2.3 Case Study: Functional Embedded Telephony in Camelot

1. 12 In addition to the primitive types supported by OCaml Camelot still provides unit type which has a single value Camelot has its own built in functions which are shown in Appendix C 2 2 2 OCamelot Object Oriented Camelot The original motivation for adding object oriented features to Camelot is the need to create a system allowing inter operation with external Java libraries and to compile an object system to JVML 21 Rather than creating a fundamentally different system the object system for Camelot is drawn from the object system of the JVM From another point of view the power of Camelot s object system might be considered as a subset of OCaml s Table 2 1 shows the basic features of Chapter 2 OCamelot Static Static methods and functions are java lang Double parseDouble a Method conceptually equal ignoring the Calls use of classes for encapsulation Static Field Only accesses to constant static java lang Double MAX VALUE Access fields are supported Object Use the new operator in the curried new java lang Double 3 1415926 creation form Retrieve the value of an instance _ object field Instance field access Update the value of an instance object field value Method introduce from OCaml s syntax object method paral para2 invocation using a curried form Considering existence of null jisnull expr Null object a function isnull is added to Test if the expression expr is a v
2. 1 Proof Carrying Code Framework The comprehension of this technology has been stated in previous sections 2 MRG Project Besides for the components introduced in section 1 3 2 MRG still made some other achievement Understanding some work of this project is required for this project 3 DEGAS DEGAS Design Environments for Global ApplicationS mainly concerns specification in UML and the qualitative and quantitative analysis of global applications In 17 DEGAS provides a case study of m MMPORG mobile Massive Multi Player Online Role Game the one to be implemented in this project in the form of a high level UML design for a room based game to be played over mobile telephones 4 Current technologies on mobile devices development This provided me ideas for later practical implementation work 1 5 Structure of the Dissertation The organization of this dissertation in chapters occurs as follows Chapter 2 This chapter first gives a literature review about OCaml and Camelot and then introduces the implementation of this game in detail Chapter 3 Work on inference of heap space usage is presented in this part But before that linear programming and a program logic are introduced first Chapter 4 This chapter concludes the work we have done for this project followed by an expectation of further work Chapter 2 Chapter 2 Camelot and the Case Study 2 1 OCaml Objective Caml OCaml Objective Caml is an advanced pro
3. concatList t Cons6 a b 12 d Figure 2 6 b A Method in the Project Using Deconstructive Pattern Match with d 28 Chapter 2 let clearStringIntList l stringintlist match l with Nil3 gt Cons3 a b t _ clearStringIntList t Figure 2 6 c A Method in the Project Using Deconstructive Pattern Match with _ Figure 2 6 Using The Diamond Type 2 Defining Our Own Classes Section 2 4 3 1 describes the layer architecture of this game From the point of implementation view each layer corresponds to a Camelot class So in the program we have three major classes reomgame class realizing the Game Engine layer userinterface realizing the User Interface connectionManager realizing the Connection Manager layer Thread connect assumes jobs like the Network Connectivity layer but we put its introduction in the next section Other than this plr class room class actually it is a Thread messageSender Thread messageReceiver Thread are assistance classes Rather than implementing the object element and the weapon element of the game as classes we design special datatypes for them in order to enable the inference experiment conducted in the next chapter Concrete definitions of object type weapon type and related datatypes are given in Appendix D 4 Figure 2 7 shows part of the declaration of the reomgame class to give a straightforward example of our usage of Camelot s OO features 29 Chapt
4. Camelot the high level language and Grail the low level language into which Camelot is compiled 1 Camelot Chapter 1 Camelot is a first order OCaml like resource safe function language which was developed as a test bed for different methods of analyzing heap usage 14 Camelot provides the usual recursive datatypes and recursive functions definitions using pattern matching albeit restricted to flat patterns 12 In order to create a system allowing inter operation with external Java libraries and to compile an object system to JVML Camelot further extends its type system to include object oriented features With respect to the concurrency problem a simplified thread model is added in Camelot which abbreviates the use of threads in the language Still Camelot has its differences from OCaml one of which lies in Camelot s memory model Through a special type Camelot enables programmers to precise control heap space usage More information about this type is put in a later section about the space aware type system And a detailed introduction to this language is in chapter 2 2 Grail Grail is a small typed language which represents Java bytecode in a functional form As a conventional strict first order functional language Grail has the following four characteristics 15 call by value function invocation lexical scoping for variables mutually recursive local function declarations strict static typing As a vehi
5. Next I will give an introduction of two different approaches which represent two directions of researches on this problem one on hardware and one on software 1 Add a limited form of virtual memory which provides memory protection but not swap space 1 This method is mostly implemented in a few high end embedded systems 2 Unlike virtual memory for desktop systems which gives programmers the illusion of an unlimited usage of memory all embedded 2 Chapter 1 systems regardless with or without virtual memory are inherently constrained by the amount of available physical memories 3 In other words because of their lack of hard disks and hence of swap space out of memory problem has not been thoroughly solved and even programs running on embedded systems that have memory management hardware and virtual memory is still possible to cause memory overflow On the other hand most commercial embedded processors such as 4 5 6 do not go in for this method The major reason for that is the cost of the hardware memory management units MMUs that provide virtual memory has been considered by processor vendor to be excessive in an embedded environment 7 1 Software run time checks for out of memory errors This method is proposed in 1 The basic idea consists of two parts First out of memory errors are detected just before they will happen by using carefully optimized compiler inserted run time check code Such error dete
6. a simplified thread model is especially designed for concurrent programming which abbreviates the use of threads in the language These derived forms are implemented by class hoisting moving a generated class definition to the 21 Chapter 2 top level of the program 20 Figure 2 4 shows concrete forms let rec threadname args let locals subexps in threadname args let threadInstance new threadname actuals in class threadnameHolder args java lang Thread with let rec threadname let locals subexps in threadname method run unit let _ this setDaemon true in threadname end let threadInstance start in Figure 2 4 Derived Forms for Thread Creation and use in Camelot 20 In order to retain predictability of memory behaviour in Camelot there are several restrictions 1 The stop and suspend methods from Java s threads API are not allowed This is because the former will cause objects to be exposed in a damaged state the latter will freezes threads without releasing resources occupied by them and as a result both of them can confuse the prediction of memory consumption 2 All threads are required to run namely all threads are started at the point where they are constructed This is also required for the sake of predictability 3 Each class has one constructor which implies that overloading is not supported by Camelot So initial values for all the fields of the class
7. int card 0 int string string it int int string 0 0 removeCard 0 cardlist 0 card 0 int string string int int int string 0 0 int cardlist 0 card 0 int string string int int int string 0 0 0 showCardList 0 cardlist 0 card 0 int string string int int int string 0 0 gt int gt int gt string gt string 0 string _of _int 0 int gt string 0 63 Chapter 3 We have noticed that most of these functions require no extra heap cell before executing and do not return any heap cell after executing So the heap space this kind of functions need relies on the size of inputs For example the sizeof function on stringpairlist it doesn t need any more heap cells during its execution except for those allocated at the beginning to hold the input stringpairlist So the number of heap cells this function needs is equal to the length of the input list It is the same to other functions which have same annotation types as sizeof There is another case shown above showStringPairList 1 stringpairlist 0 string string 0 gt int gt int gt string string 1 ssElementAt 1 stringpairlist 0 string string 0 int gt stringstringpair 1 string string 0 0 2 The type for showStringPairList says that it needs at least one free heap cell before starting and leaves at least one free cell on the heap when it returns This heap cell is used up i
8. lt 10000 a02 lt 10000 u01 lt 10000 u02 lt 10000 x01 lt 10000 Figure 3 5 simple constraints All constraints for Inference The linear problem we pick out from it is Minimize 4 u01 4 u02 2 x01 1 y01 Subject to hd 11 Val 1 a02 1 yOl lt 0 1 hd 11 M 2 1 a02 1 u02 1 x01 lt 0 2 hd 10 Val 1 a01 1 yOl lt 0 3 hd 10 M i 1 a0 1 1 u01 1 x01 lt 0 4 a01 a02 u01 u02 x01 yOl gt 0 51 Chapter 3 a01 a02 u01 u02 x01 y01 lt 1000 is the upper bound which are predefined by the system Add 1 and 2 to remove a02 and the same to 3 and 4 to remove a01 we can get Minimize Z 4 u01 4 u02 2 x01 1 y01 Subject to y01 u02 x01 lt 0 y01 u01 x01 lt 0 u01 u02 x01 y01 gt 0 Then we will use the Simplex Method introduced in Section 3 1 to find the optimal solution for this problem Step 1 Introduce slack variables to the constraints and rewrite the objective function in standard form u02 x01 y01 s01 0 u01 x01 y01 s02 0 4u01 4u02 2x01 y01 Z 0 Step 2 Write down the initial tableau Step 3 Select the pivot column For this example the pivot column is y01 column Step 4 Select the pivot in the pivot column Cons1 0 1 1 1 0 0 0 0 1 0 Cons2 1 0 1 0 1 0 0 0 1 0 Min 4 4 2 0 0 1 0 52 Chapter 3 So we pick up the 1 in the first row as the pivot Step 5 Use the pivot to
9. user login logout and account management In the logic of the Game the Server has only little participation instead the Client takes on most of these jobs Figure 2 5 shows the structure of the application on the Client side followed by Table 2 3 explaining the work of each layer User Interface J Security Figure 2 5 Layered Architecture Chapter 2 Layer Duty User Interface Enable user to interact with the game Game Engine Implement all the game logic i e actions of the l player Communication implement all the communication activities of the game i e p2p client server communication Network Connectivity rovide essential Network Connectivity allowing the system to relay on an appropriate transfer protocol i e HTTP Security Support On the 3rd and 4th layers provide necessary security need to be improved support for communication applications and ee a connectivity between peers Table 2 3 Explanation of the Game Architecture 2 4 3 2 Major Implementation Issues In the previous section we have pointed out that this is a distributed system Issues discussed in this section relate to this feature 1 Mobility amp Distributed Environment This system is highly mobile and has a P2P nature Players inside a Room constitute a virtual community that they can join and leave and interactions between them can only occur inside the same room Room object is the most important mo
10. 1 12 July 2004 89 23 24 25 26 27 28 29 Bibliography M Hofmann and S Jost Static Prediction of Heap Space Usage for First order Functional Programs In Proceedings of the 30th ACM Symposium on Principles of Programming Languages ACM Press New York Vol 38 No 1 pages 185 197 January 2003 Srinath L S Linear Programming Principles and Applications 2 Edition book David Aspinall Lennart Beringer Martin Hofmann Hans Wolfgang Loidl and Alberto Momigliano A program Logic for Resource Verification In Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics TPHOLs2004 Springer Verlag LNCS Heidelberg Vol 3223 pages 34 49 September 2004 M Hofmann and S Jost Static Prediction of Heap Space Usage for First order Functional Programs In Proceedings of the 30th ACM Symposium on Principles of Programming Languages ACM Press New York Vol 38 No 1 pages 185 197 January 2003 Lennart Beringer Martin Hofmann Alberto Momigliano and Olha Shkaravska Towards Certificate Generation For Linear Heap Consumption In Proceedings of ICALP LICS Workshop on Logics for Resources Processes and Programs LRPP2004 July 2004 Steffen Jost lfd_infer an Implementation of a Static Inference on Heap Space Usage Inst for Informatics LMU Univ Munich Nicholas Wolverson and Kenneth MacKenzie O Camelot Adding Objects to 90 Bibliography a Reso
11. 1 June 2003 88 16 17 18 19 20 21 22 22 Bibliography MRG Report Information Society Technologies IST Programme Annex Description of Work October 2004 http groups inf ed ac uk mrg project info contract new pdf C Caragiuli D Piazza I Mura C Chesta G Previti and M Di Florio D24 Specification in UML of Case studies In Design Environments for Global ApplicationS DEGAS IST 2001 32072 pages 6 12 17 21 34 61 31 December 2002 Wikipedia The Free Encyclopedia http en wikipedia org wiki Main Page Xavier Leroy The Objective Caml system release 3 08 Document and User s manual July 13 2004 http caml inria fr pub docs manual ocaml index html S Gilmore K MacKenzie and N Wolverson Extending Resource Bounded Functional Programming Languages with mutable state and concurrency In Parallel and Distributed Computing Practices pages 1 19 2005 Hans Wolfgang Loidl and Kenneth MacKenzie A Gentle Introduction to Camelot LFCS Univ of Edinburgh amp Inst for Informatics LMU Univ Munich pages 1 36 September 2004 Kenneth MacKenzie An Overview of Camelot LFCS Univ of Edinburgh pages 1 11 3 July 2003 Lennart Beringer Martin Hofmann Alberto Momigliano and Olha Shkaravska Towards certificate generation for linear heap consumption In Proceedings of ICALP LICS Workshop on Logics for Resources Processes and Programs LRPP2004 pages
12. 8 George C Necula Peter Lee Safe Untrusted Agents using Proof Carrying Code In LNCS 1419 Special Issue on Mobile Agent Security Springer 1998 87 9 10 11 12 13 14 15 Bibliography George C Necula Peter Lee Safe Kernel extensions without run time checking In Proc 2 USENIX Symp On Operating System Design and Impl pages 229 243 1996 George C Necula Proof Carrying Code In Proc 24 ACM Symp On Principles of Prog Lang pages 106 119 New York Jan 1997 ACM Press Andrew W Appel Foundational Proof Carrying Code In LICS 01 16 Annual IEEE Symposium Logic in Computer Science pages 1 10 June 16 2001 David Aspinall Stephen Gilmore Martin Hofmann Donald Sannella and Ian Stark Mobile Resource Guarantees for Smart Devices In Construction and Analysis of Safe Secure and Interoperable Smart Devices Proceedings of the International Workshop CASSIS 2004 Springer Verlag No 3362 pages 1 26 2005 MRG Final Report 30 June 2005 http groups inf ed ac uk mrg project info final report pdf Kenneth MacKenzie and Nicholas Wolverson Camelot and Grail resource aware functional programming on the JVM In Trends in Functional Programing Intellect Vol 4 pages 29 46 2004 Lennart Beringer Kenneth MacKenzie and Ian Stark Grail a Functional Form for Imperative Mobile Code In Foundations of Global Computing Proceedings of the 2nd EATCS Workshop Elsevier No 85
13. Let in a particular problem the constraint condition appear as AX AX 4 X lt b ip By adding a suitable positive quantity x to the left hand side the two sides can 1 be equated therefore the inequality constraint can be written as 36 Chapter 3 AX a X a X Xp H If the constraint condition appears with a greater than or equal to sign this can also be changed into an equation by subtracting the positive quantityx from the p l left hand side aX a X A X Ky b This standard form is adopted in the simplex method which is a widely used solution algorithm for solving linear programs In the experiment section we will use the simplex method to solve a linear programming problem generated by the type system and the specific problem logic 3 2 The Program Logic The program logic for reasoning about resource consumption of programs written in Grail is one of the essential components of the MRG project The introduction to the program logic in this section will be based on 25 26 27 Serving as the target logic of a certifying compiler the program logic exploits Grail s dual nature of combing a functional interpretation with object oriented features and a cost model for the JVM 25 This program logic together with the resource aware operational semantics of Grail has been formalized in the theorem prover Isabelle HOL The logic exists not only on the code producer
14. Otherwise the method will be assumed to be monomorphic and given an incompatible type 19 OCaml provides the library function Oo copy for cloning objects Usually the instance variables have been copied but their contents are shared Assigning a Chapter 2 new value to an instance variable of the copy will not influence the original s and vice versa However in the case that the instance variable is a reference cell assignments will influence both the original and the copy OCaml allows recursive classes definitions where recursive classes can be used to define objects whose types are mutually recursive OCaml provides a novel method the binary method which takes an argument of the same type as self 2 2 Camelot Camelot serves as the high level programming language in MRG framework Owing to its resource safe character it is developed as the test bed for different methods of analyzing heap usage 2 2 1 The Core Language Comparison between Camelot and OCaml The core of Camelot is a standard polymorphic ML like functional language whose syntax is based upon that of OCaml 20 In section 2 2 we have introduced the core language of OCaml so here we only focus on differences between them Appendix C shows the complete syntax of Camelot 1 In OCaml there is actually no way to modify a list in place once it is built For example the sort function in figure 2 1 a does not modify its input list instead it
15. free var expr match mrule match mrule oe con pat pat gt expr con Clone pat pat gt expr pat vra In some contexts the symbol _ can be used instead of a variable name This feature can be used to discard unwanted values 72 Appendix C Appendix C Camelot s Built in Funtions There are some built in functions provide by Camelot The names of most of these are self explanatory int_of_float float gt int float_of int int gt float int_of_string string gt int string of int int gt string float_of_ string string gt float string of float float gt string print_ int int gt unit print int newline int gt unit print float float gt unit print_float_newline float gt unit print_char char gt unit print char newline char unit print string string unit print string newline string unit print_newline unit gt unit same_ string string string bool Array operations empty int gt a gt a array get amp array gt int gt amp set array gt int gt unit arraylength array int 73 Appendix D Appendix D 1 The Map of The Game The game consists of a series of game levels Each level is composed of a start area a certain number of standard rooms and a special room which can hold only one player at a time Level Level Level E EE essen busch secs ach tuted A EE Start Are a 74 Appen
16. may request to take objects or weapons from the same room at the same time The system must notice this race and grant exclusive access to these resources And the way to do this is implementing the Token as briefly described above The token can be thought of as a mobile object moving from one peer to another peer in the same room Only the player owning the Token can access resources and perform the action he requested Other players must wait and their requests will be stored in a queue of the Token After the peer has finished processing the action the new status of the room needs to be broadcasted to all the other peers in the room for the sake of keeping the consistency of the room Those peers receiving the information must update their clone of the room object After this procedure has succeeded the Token can move somewhere else On the other hand the request of the other peer will be enqueued and after the action is finished the request will be dequeued In addition to these two issues the design of the database is also a concern of this project Appendix E 7 shows the E R diagram of this project 2 4 3 3 Programming in Camelot This case study takes full advantage of the facilities provided by Camelot i e 27 Chapter 2 diamond type for heap space allocation self defined classes threads for concurrency and so on Therefore it s a good opportunity to help test and the Camelot compiler 1 Using the Diamond Type Diamond typ
17. methods for multiple threads memory usage need to be considered Table 3 4 concludes solutions for this problem proposed in 20 48 Chapter 3 Approach Description Strongpoint Shortcoming Shared A single free Efficient memory usage Run time penalty caused by free list list of synchronization an storage is overhead of locking and shared across unlocking the parent of the all threads field occurs when entering and leaving a critical section Private Each thread No requirement for access Memory use penalty free list separately to the free list to be There will be times when maintains its synchronized therefore one thread allocates own local time is saved memory while another instance of thread has unused memory the free list on its local free list Hybrid Each thread Reduce the overhead of The analysis of this free list has a local calls to access the approach is complicated free list synchronized global free meanwhile a list while preventing global free threads from keeping too list exits as many unused memory cells well locally Table 3 4 Solutions for the Heap Usage Problem of Multi Threads Camelot chooses the first scheme In addition to it a requirement is imposed to ease the predictability of memory usage which is that data structures in a multi threaded Camelot program are not shared across threads This requirement means that the space consumption of a multi threaded Camelot program is obtained as th
18. name weapon 81 Appendix E type cardlist Nil2 Cons2 of weapon weaponlist type card NullWeapon Weapon of int string string int int int string let cid w match w with Card id _ _ _ id NullCard 0 let cname w match w with Card _ name _ _ gt name NullCard gt let figure w match w with Card _ _ fpath _ _ fpath NullCard gt let attAbility w match w with Weapon _ _ _ attak attak NullWeapon 0 let defAbility w match w with Card _ _ _ _ defence _ defence NullCard 0 let condition w match w with Card _ _ _ _ _ cond gt cond NullCard gt let cardElementAt l cardlist k match with Nil2 NullCard Cons2 h t gt if k gt 0 then cardElementAt t k 1 else h let cardListLength l cardlist match with Nil2 gt 0 Cons2 h t gt 1 cardListLength t 82 Appendix E let findCard l cardlist id int k int n int card if k lt n then begin let weapon cardElementAt l k in if id cid weapon then weapon else findCard I id k l n end else let weapon NullCard in weapon let concatCardList l cardlist k int n int sink string ifk lt n then let cardIns cardElementAt l k in let sink sink string _of _int cid cardIns cname cardIns figure cardIns string _ of _int attAbility cardIns string _of _int defAbility
19. need to be passed when an object is created 22 Chapter 2 2 3 Case Study Functional Embedded Telephony in Camelot This is a case study project to develop an on line game application in the Camelot programming language The design of the game is based on 17 where DEGAS provides a case study of m MMPORG in the form of a high level UML design for a room based game to be played over mobile telephones The motivation of this part is to implement a large practical system in Camelot taking advantage of the features of this language as well as to test Camelot compiler 2 3 1 Game Storyline This Massive Multi Player Online Role playing Game MMPORG consists of a series of game levels Each level is composed of a start area a certain number of standard rooms and a special room which can hold only one player at a time The architecture of every level is different from level to level this means that the number of rooms and the paths they are connected by may change Appendix D 1 shows the map of this game Each player in the game has four associated parameters health strength agility and cash Players are considered as active entities who can operate on objects change locations interact with other players and so on Allowed actions are listed in Appendix D 2 with necessary explanation Objects including food weapons medicine tools etc are divided into categories according to the player s parameter they affect Object Categor
20. poq COMP Eth snd FT f h v p Eth call f U h v 1 0 0 0 p FT the function table used to obtain function bodies from names CALL newframe null fst MT c m a E th snd MT c m y h v p al 01 i e p MT the method table used to obtain method bodies from names SINV EHh cOm a h v 2 newframe creates an appropriate environment classOf E hxc newframe E x fst MT c m a E Hh snd MT c m h v p Eth xem a U Thsvs 4 al 01 ie pj classOf retrieves the dynamic class name c associated to the object pointed to by x Figure 3 3 The Dynamic Semantics of Grail 41 VINV Chapter 3 Component Representation a global abstract instruction counter the number of function calls jump instructions the number of method invocations invkdpth the maximal invocation depth Table 3 2 Representation of Resource s Four Components clock U point wise addition callc Oy U point wise addition invkc U point wise addition point wise addition invkdpth U pick the maximum Table 3 3 Operations on Resource Notice that instead of being explicitly recorded in the resource model the size of heap is deduced from dom h which represents the domain of the object heap 3 2 2 The Program Logic The MRG project employs the Proof Carrying Code infrastructure which equips Grail programs with certificates concerning their resource consumption Certificates
21. programs The formal syntax of Grail is shown in figure 3 2 25 followed by a table explaining symbols appearing in the syntax aeargs varx null i eeexpr null inti var x prim op x x new c e x x t aL cot Oot x letx e ine e e if x then e else e call f xem a cO m a Figure 3 2 The Syntax of Grail 38 Chapter 3 Name Representation x i op null x t xX t y COK x let x e in e2 C13 amp 2 Variable Integer Method Name Class Name Function Name i e labels of basic blocks static field names primitive operator V gt V gt V i e arithmetic or comparison operator Semantic category of values Comprising integers references r and the special symbol L absence of a value Null Heap Reference Same as the non static getfield instruction Same as the non static putfield instruction Same as the static getfield instruction Same as the static putfield instruction The evaluation of e returns an integer or reference value on top of the JVM stack Sequential composition new c t Xj n Xn Create and initial an object of class c according to the call f c m a x m a argument list Function call i e immediate jumps without arguments Static method invocation Instance method invocation Table 3 1 Explanation of Grail s Syntax 39 Chapter 3 Operational semantics of Grail based on its functional interpretation are shown in fi
22. return type of clearObjectList is unit 0 The 0 will at least be a correct bound for the amount of heap space obtained when we call clearObjectList To get a correct answer we d need a type like 56 Chapter 3 unit n where n is the length of the input list But Ifd_infer s type system currently cannot express this Therefore the memory leak in lfd_infer sometimes is not a memory leak However in order to pass the inference of lfd_infer we modify the code a little type objectlist Nil Cons of obj objectlist type obj NullObject Object of int string int int string let clearObjectList l objectlist match l with Nil gt Nil Cons h t _ gt Cons NullObject clearObjectList t The modification seems artificial Since constructor NullObject takes no space this function uses the same heap space as the original one But the Ifd_infer passes it first because the second Cons could subsequently gain the reference released by the destructive pattern match and second because the return type is objectlist rather than unit We use the same trick to solve the memory leak reported when we analyse other programs Problem 3 Unbounded Heap Usage Reason Ifd_infer When parsing stringpairlist cmlt and stringintlist cmlt we get LFD types suck as the following taking function siElemenetAt in stringintlist cmlt for example siElementAt 10000 stringintlist 0 string int 0 int stringintpair 1000
23. side where it is used by the certifying compiler to generate certificates but also on the code consumer side where it is used by the proof checker to check whether the certificate attached to the code indicates that the required resource of the program will not violate the resource policy the consumer claimed and whether this certificate is logically correct This project uses the Hofmann Jost type system to provide quantitative guarantees about the resource consumption The concern of this type system is that given a functional program containing a function f of type say L B gt L B i e turning 37 Chapter 3 lists of Booleans into lists of Booleans find a function v such that the computation f w requires no more than v w additional heap cells 25 By encoding a Grail level interpretation of the Hofmann Jost type system a smooth transition from program analysis to program verification can be obtained 3 2 1 The Syntax and Operational Semantics of Grail The main characteristic of Grail is its dual identity its impure call by value functional semantics may be shown to coincide with an imperative interpretation of the expansion of Grail programs into the Java Virtual Machine Language provided that some mild syntactic conditions are met 27 Certificates expressed in the program logic are obtained by computing in Isabelle HOL some resource properties of heap manipulating Grail programs that were produced by compiling Camelot
24. string 0 int 0 cardElementAt 0 cardlist 0 card 0 int string string int int int string 0 0 gt int gt card 0 int string string int int int string 0 0 cardListLength 0 cardlist 0 card 0 int string string int int int string 0 0 gt int 0 cardOwner 0 card 0 int string string int int int string 0 string 0 cid 0 card 0 int string string int int int string 0 int 0 clearCardList 0 cardlist 0 card 0 int string string int int int string 0 0 cardlist 0 card 0 int string string int int int string 0 0 0 cname 0 card 0 int string string int int int string 0 string 0 concatCardList 0 cardlist 0 card 0 int string string int int int string 0 0 gt int gt int gt string gt string 0 condition 0 card 0 int string string int int int string 0 int 0 copyCardList 0 cardlist 0 card 0 int string string int int int string 0 1 gt cardlist 0 card 0 int string string int int int string 0 0 gt cardlist 0 card 0 int string string int int int string 0 0 0 defAbility 0 card 0 int string string int int int string 0 int 0 figure 0 card 0 int string string int int int string 0 string 0 findCard 0 cardlist 0 card 0 int string string int int int string 0 0 gt int gt int gt
25. this project faces a variety of problems Thus it is a good opportunity to test and improve the Camelot compiler so this is the other task of this project Acknowledgements First I would like to thank my supervisor Professor Don Sannella for his continued guidance and many fruitful discussions throughout the project and Dr Kenneth MacKenzie this work would not have been possible without his insightful help I would also like to thank Dr David Aspinall for his helpful advice and encouragement Thanks also to my family and friends for providing support and encouragement throughout my entire MSc Declaration I declare that this thesis was composed by myself that the work contained herein is my own except where explicitly stated otherwise in the text and that this work has not been submitted for any other degree or professional qualification except as specified Hua Yang ili Table of Contents Chapter 1 Introduction oe soeosseosseossoossoossssesssesssoossoossoossssesssesssocssoosssssssosssseessoosso 1 1 1 Embedded System Development scar cseiss tive nacsinaieanssaenisesntsenen cuss 1 1 1 1 Memory Overflow Coneettticssiiiciancasdiietiiss canines Gackn 1 1 1 2 Related Work on Memory Overflow Problem c eeeeeteees 2 1 2 Proof Ga rtyimg Code sug hase yarascascticaa ian eb yeas eee GeO 3 1 7 gt MRG PROJ CCE dara tas chalet ereen t canes eee aut a caitagg ae onde EEn ee R NEEE E 6 1 3 1 Architecture
26. with the resource aware operational semantics of Grail has been formalized in the theorem prover Isabelle HOL Certifications in the MRG framework contain a claim of resource usage together with a proof of the claim And this proof is just expressed in this program logic The logic exists not only on the code producer side where it is used by the certifying compiler to generate certificates but also on the code consumer side where it is used by the proof checker to check whether the certificate attached to the code indicates that the required resource of the program will not violate the resource policy the consumer claimed and whether this certificate is logically correct A detailed introduction to this will be given in Chapter 3 1 4 Description of the Project 1 4 1 Motivation and Description of the Project In these years the worldwide market of mobile communication is growing at a rapid pace and has overtaken wired phone communications We have heard for a while that the mobile industry will explode with millions of end user playing games and interacting on billions of handsets In particular Screen Digest June 2004 estimated that the total market for online games will double between 2004 and 2007 the Massive Multi Player Online Game MMOG market continues to grow and Chapter 1 Europe a relatively untapped MMOG market to date will become the largest growth opportunity when the North American market approaches saturation On t
27. 0 string int 9999 0 This means that the heap space required by function siElemenetAt is unbounded when it starts executing as 10000 is the default highest value of the number of heap cells available From the view of linear programming we can use the following figure 3 6 to explain this unboundedness problem As we can see it is impossible for the objective function to find a point of intersection with either constraint inequality in the feasible region within a finite value In this case Ifd_infer just 57 Chapter 3 simply assumes that the consumption reaches the upper bound and this is why we see 10000 or 9999 in the LFD type In order to obtain a finite solution the programmer has to use the options olhs orhs odin odout provided by lfd_ infer to change the objective function himself Figure 3 7 shows how this change works For our program after using option olhs 4 we can get a reasonable LFD type siElementAt 1 stringintlist 0 string int 0 int stringintpair 1 string int 0 0 Although the problem is solved finally the penalty for it is that programmers themselves have to manually change the objective function so as to get a reasonable solution This obviously imposes a burden on the programmer constraint ine feasible region constraint inequality 1 objective function Figure 3 6 An Unbounded Case in Linear Programming 58 Chapter 3 constraint ine feasible re
28. 4y subject to 3x 4y lt 12 x 2y24 x21 y20 The feasible region for this set of constraints is shown below feasible Figure 3 1 Feasible Region for LP Program The following table shows the value of Z at each corner point Point Z 3x 4y 1 1 5 3 1 4 1 5 9 minimum 4 0 3 4 4 0 12 35 Chapter 3 Therefore the solution is x 1 y 1 5 giving the minimum value Z 9 The graphic method can only effectively solve those linear programming problems involving two variables Usually all minimization problems can be expressed in a standard form as follows 24 Determine x 20 x 20 x 20 3 1 so as to minimize Z c x x X 3 2 subject to the constraint conditions expressed as equalities aX tax a x D Ay X A X 4 x D TA DX tapX H F Ann X b m2 mn n m The constants c j 1 2 n in the objective function are called cost coefficients the constants b i 1 2 m defining the constraint requirements are called stipulations and the constants a i 1 2 m and j 1 2 n are called structural coefficients The sign conditions imposed by 3 1 are known as the non negativity requirements In practice the constraint conditions generally appear as inequalities with greater than or less than signs or in a mixed form In order to replace the inequalities constraint conditions by constraint equations slack variables which are positive are introduced
29. Chapter 1 Figure 1 2 shows MRG s PCC like architecture Along with it is a novel protocol proposed by MRG In this protocol a Resource Manager is responsible for negotiating resource policies specified by the code consumer with the code producer and verifying that the certificate attached to the required code ensures that it will run within the constraints required A Proof Checker invoked by the Resource Manager is in charge of the practical verification work If the check succeeds we have an absolute guarantee that resource bounds are met so it is not necessary to check for resource violations as the code runs In detail the phases in the protocol are 16 Initiate Code producer A wants to send code consumer B a piece of mobile code c Policy A and B agree upon some resource policy r that the code must satisfy The choice of policy may influence some aspect of the compilation or re compilation of the code from a high level language in particular how the Resource Type checker influences the Certificate Generator Certify Provided the code meets the policy r then A sends B the code c together with a certificate p that c abides by r Check B checks the validity of the certificate p with respect to the code and the agreed resource policy Run Provided the check was successful B then runs the code 1 3 2 Components of MRG 1 3 2 1 Programming Languages The Mobile Resource Guarantees framework provides two language levels
30. Functional Embedded Telephony in Camelot elie Hua Yang Master of Science School of Informatics University of Edinburgh 2005 Abstract This project would first develop an on line game application in the Camelot programming language which would be compiled to run on an emulator for a Java enabled mobile phone Java enabled mobile telephones allow users to develop and download their own code onto the handset Programming an embedded system such as a telephone is very different from programming a general purpose workstation Embedded system developers face problems such as conserving the battery life which have no analogue in traditional desktop computing One of the most significant costs of battery energy in embedded devices is memory usage For this reason developers benefit from using Camelot an OCaml like functional programming language which can give precise guarantees of resource consumption inferred directly from the application code Camelot uses the Hofmann Jost type system to provide quantitative guarantees about the consumption of resources such as memory And Ifd_infer is the implementation for the static prediction of heap space usage which relates to the Hofmann Jost type system This project will use this tool to get the resource consumption of the game On the other hand although Camelot has been used in a wide range most implementations of it so far are small and aim for particular problems The implementation of
31. However the inference will fail if such functions are called by any other declared and defined function of the program On the contrary any defined function is checked based on their given declaration If a function is undefined then all the annotations related to it are assumed to be zero or accepted as given We have mentioned Ifd_infer s enriched typing above which calculates resource annotations for functions and is therefore able to provide programmers with helpful information on resource assumption analysis This annotated type is like this 46 Chapter 3 insert 1 int Jist Nil 0 Cons int 0 gt list Nil 0 Cons int 0 0 where for each occurring type all its constructors are listed and for each constructor a number indicating the amount of heap cells that must be supplied for each node contained in the input of that type is added The first hand information from the annotated type is that at most how many heap cells are required at the beginning for the sake of normally starting and executing a function and that how many heap cells will be returned after its execution So for example the type above says that a call to insert may allocate one heap cell during its execution and do not return any heap cell after executing On the other hand Ifd_infer has an obvious deficiency which was also admitted by its creators Leaving programmers to designate for each pattern match whether it is destructive or not
32. a specific user interface package which can ease our work in the future 2 Game Security 17 proposes a Wide Mouthed Frog algorithm for this problem based on the SSL protocol M created Kap Kap a A F Protocol Narration S 1 A gt S M A Kas B Kas 2 SSB Keps A Kap Kas 3 ADB Kapil M B Figure 4 1 the Wide Mouthed Frog Algorithm 17 The figure above shows the details of this algorithm to establish a secure connection between peer A and peer B First peer A creates the key Kap he wants to use to talk with B then sends this information through a secure connection to the Server using his session key KAs The Server forwards the information directly to B using their session key Kgs Now that B has the session key Kap A can encrypt message M using private session key Kag and send it to B Now that peer A and B have established their private session key they can have secure communication without relaying to the Server anymore 3 The program logic The program logic is used to assert resource related properties of Java bytecode programs Currently we can get the inference of heap space usage for our program those pure Camelot codes in the program which forms part of the certification It is nevertheless worthwhile to experiment with 68 Chapter 4 another part of the certification the proof at the bytecode level Moreover using the raw proof rules at the bytecode level will enable proofs to be given that are n
33. able data structures such as arrays 19 Like ML OCaml also provides exception signaling and handling mechanism 2 1 1 2 The Module System The module system is one of the important characteristics of OCaml The primary motivation for it is to centralize related definitions e g definitions of a data type and associated operations on that type as well as enforce a consistent naming scheme for these definitions This can efficiently avoid running out of names or accidentally confusing names 19 Structures Signatures and Functors form the basis of this system 2 1 2 Object Oriented Features of OCaml OCaml supports class definition Like conventional object oriented programming languages OCaml provides concepts like private methods abstract methods but here called virtual methods inheritance class coercions friend class as well as new for creating objects Features of OCaml which distinguish it from OO imperative languages are OCaml provides a direct way to create an object without going through a class The syntax is exactly the same as for class expressions but the result is a single object rather than a class Unlike classes which cannot be defined inside an expression immediate objects can appear anywhere using variables from their environment 19 In the body of a class polymorphic methods are allowed but with a limitation namely a polymorphic method can only be called if its type is known at the call site
34. airl of string int let siElementAt l string intlist k match with Nil3 Nonel Cons3 a b t if k gt 0 then siElementAt t k 1 else Pairl a b let lengthof L string intlist match l with Nil3 gt 0 Cons3 a b t gt 1 lengthof t 80 Appendix E let removeFirst l string intlist match with Nil3 gt Nil3 Cons3 a b t gt t let findRoom l string intlist direction string int match with Nil3 gt 0 Cons3 a b t gt if a direction then b else findRoom t direction let concatStringIntList l string intlist k int n int sink string string ifk lt n then match siElementAt l k with Pairl key value _ gt let snk sink key string of _int value in concatStringIntList k 1 n sink Nonel gt sink else sink let copyStringIntList 11 string intlist 12 string intlist match Il with Nil3 gt 12 Cons3 a b t gt let 12 Cons3 a b 12 in copyStringIntList t 12 let showStringIntList l string intlist k int n int sink string string ifk lt n then begin match siElementAt k with Pair key value gt let snk sink key string _ of _int value n in showStringIntList k 1 n sink Nonel gt sink end else sink let clearStringIntList l string intlist match with Nil3 gt Cons3 a b t gt clearStringIntList t cardlist cmlt At the very beginning we used card to
35. alues test whether the curried expression null value is a null value cast objects up to superclasses obj gt superclass Casts amp cast objects down to subclasses match obj with typecase o gt subclass 0 a o gt subclass2 o b __ obj c Table 2 1 Basic Features of Camelot s Object System In addition OCamelot also supports self defined classes This facility can be used to implement callbacks such as in the Swing GUI system which requires us to write stateful adaptor classes 29 or to invoke Camelot codes in the context of Java for Chapter 2 example to create a resource certified library for use in a Java program 29 Figure 2 3 shows the syntax of a class declaration followed by table 2 2 explaining items in the syntax Examples of self defined classes can be found in the next section which introduces implementation details of this project Clearly the presence of mutable objects in object oriented Camelot provides for in place update 29 However the unbounded heap usage problem solved for datatypes are replicated by allowing arbitrary object creation Perhaps more seriously invocating arbitrary Java code in Camelot programs may lead to unlimited heap space usage Further discussion about this problem will be given in chapter 3 classdefl class cname scname with body end body interfaces fields methods interfaces implement iname interfaces fields field fie
36. ay not want to re use a diamond value immediately a freelist is provided for the storage of unused diamonds The type system provides two ways to achieve linear typing First the Camelot compiler has an option that enforces linear use of all variables or alternatively the programmer himself ensures that the datatype he deconstructed using the match rule is not used anymore because its contents will be overwritten subsequently Linear typing schemes guarantee single threadedness and so the soundness of in place update with respect to a functional semantics 37 However this is a restrictive discipline in practice and rules out many sound programs So in 37 an improved type system that distinguishes between modifying and read only access to a data structure and in particular allows multiple read only accesses is proposed 12 Chapter 1 1 3 2 3 Program Logic for Generating and Checking Proofs The Camelot programming language is supported not only by a strong expressive type system but also by a program logic which supports reasoning about the time and space usage of programs in the language Actually speaking the program logic operates on programs written in Grail which is the target of Comelot s compiler Serving as the target logic of a certifying compiler the program logic exploits Grail s dual nature of combing a functional interpretation with object oriented features and a cost model for the JVM 25 This program logic together
37. ays One is that additional space on hard disks can be provided by virtual memories the time a workload runs out of physical main memory DRAM and as a result the workload can continue making progress The second is related to the hardware assisted segment level protection mechanism provided by virtual memory which ensures that an application with an excessive memory requirement can be terminated by user without crashing the system 1 Embedded systems on the other hand typically have neither hard disks nor virtual memory support This means that out of memory errors leave the system in greater peril More specifically since there is no swap space the additional space allocated in the hard disk by the virtual memory the memory overflow application has no space to grow into therefore the system crashes Furthermore because of the absence of protection given by the virtual memory there is a possibility that a segment exceeds the memory bound cannot be detected and hence no pre crash remedial action can be performed So for correct execution programmers need to make accurate compile time estimates of the maximum memory requirement of each task across all input data sets and choose a physical memory size larger than the maximum memory requirement of the embedded application 1 1 2 Related Work on Memory Overflow Problem Currently works on the memory overflow problem have already been carried out and some helpful solutions were proposed
38. bile object of the system This object contains all the information about the virtual environment in which players are playing and provide necessary services for players during the game When entering a room of the game every player receives a copy of the Room object If the entering player is the first one in a room it is the server that creates and sends a room copy to the player s device Other players will be forwarded to players already inside the room and a peer to peer procedure will allow the newcomer to receive its copy of the Room object from some other player These 26 Chapter 2 instances of the Room object must be kept synchronized in order that every player has the same version of the status of the Room he is in This problem is solved by introducing a second mobile object a Token Each room has only one Token and only the player holding the Token has the right to perform any Environment Action The definition of Environment Action is given in Appendix D 2 If any other player wants to do some Environment Action before he can be satisfied the Token must move to the requesting player s device first 2 Synchronization Environment Actions are defined as Local and Synchronous Actions It means that this kind of actions is performed directly on the local device of the player doing them but before this is done players must synchronize on something Room is the obvious synchronized point in this game For example several players
39. bj objectlist type cardlist Nil2 Cons2 of card cardlist type string intlist Nil3 Cons3 of string int string int list type stringpairlist Nil4 Cons4 of string string stringpairlist type string int pair Pairl of string int type stringstringpair Pair2 of string string type stringlist Nil5 Cons5 of string stringlist type obj Object of int string int int string type card Card of int string string int int int string Note that the object element and the weapon element of the game are defined as datatypes rather than classes 77 Appendix D Appendix D 5 E R Diagram Of the Database This is the E R diagram for the database used on the Server side oid Comme Casi Cowned object Conan lt B gt Gr A lt Loon gt Creat Eno ED lt gt J vere Casility connect_to connect_ from C cash own_weapon See ad cid C ename gt def ability 78 Appendix E Appendix E Pure Camelot Code in the Game Declarations of functions here are the very original ones so they still have problems mentioned in chapter 3 Refer to chapter 3 to find how to modify them Stringpairlist cmlt type stringpairlist Nil4 Cons4 of string string stringpairlist type stringstringpair None2 Pair2 of string string type stringlist Nil5 Cons5 of string stringlist let ssElementAt l stringpairlist k match with Nil4 None2 Cons4 a b t gt if k gt 0 th
40. builds and returns a new list containing the same elements as the input list in ascending order Most OCaml data structures like list are immutable except for a few like arrays which can be modified in place at any time However Camelot allows in place modification through the diamond type and the freelist The diamond type in Camelot is denoted by lt gt whose values represent blocks of heap allocated memory Camelot allows explicit manipulation of diamond Chapter 2 objects and that is achieved by equipping constructors and match rules with special annotations referring to diamond values 14 See the insertion sort example in figure 2 1 c The annotation d on the first occurrence tells the compiler that the space used by the list cell is to be made available for re use via the diamond value d 22 And the second annotation on the second occurrence points out that the new list cell should be constructed in the diamond object referred to by d Considering that sometimes we don t want to re use a diamond value immediately Camelot provides a freelist for the storage of unused diamonds The diamond annotated by _ will be placed on the freelist for later use Figure 2 1 b shows the usage of it The related topic about static inference of heap space usage will be discussed in chapter 3 let rec sort l match with gt hd tl gt insert hd sort tl and insertal match with gt a hd tla if a
41. cardIns string _of _int condition cardIns in concatCardList l k 1 n sink else sink let copyCardList Il cardlist 12 cardlist match Il with Nil2 12 Cons2 a t gt let 12 Cons2 a 12 in copyCardList t 12 let showCardList l cardlist k int n int sink string string ifk lt n then begin let cardIns cardElementAt k in let sink sink cname cardIns Attack Ability gt string _of _ int attAbility cardIns Defend Ability gt string _of _ int defAbility cardIns n in showCardList l k 1 n sink end else sink let clearCardList l cardlist match with Nil2 gt Cons2 h t _ clearCardList t 83 Appendix E let removeCard l cardlist id int cardlist match with Nil2 gt Nil2 Cons2 h t h _ gt if cid h id then Cons2 NullCard t else Cons2 h removeCard t id objectlist cmlt type objectlist Nil Cons of obj objectlist type obj NullObject Object of int string int int string let oid o match o with Object id _ _ _ _ id NullObject 0 let oname o match o with Object _ name _ _ gt name NullObject gt let category o match o with Object _ _ cat _ _ cat NullObject 0 let ability o match o with Object _ _ _ abi _ abi NullObject 0 let owner o match o with Object _ _ _ _ 0wn gt own NullObject gt let objElementAt l objectli
42. class java lang Thread However in this project 30 Chapter 2 we use the Java APIs provided by J2ME instead of J2SE the former is much smaller than the latter Some of the methods defined in J2SE are not included in J2ME and java lang Tharead setDaemon is one of these There is no java lang Thread setDaemon defined in J2ME s Thread class Therefore we have to use Camelot s standard form for class definition to define treads in our game Figure 2 8 shows the definition of connect class connect java lang Thread with field url string field c javax microedition io HttpConnection field connM connectionManager field tag int maker cManager connectionManager urlocation string cTag int let _ connM lt cManager inlet _ url lt urlocation inlet _ tag lt cTag in method run unit let tag this tag in let conn javax microedition io Connector open this url in let _ match conn with hconn gt javax microedition io HttpConnection gt let c lt hconn inlet _ this c set RequestMethod Javax microedition io Http Connection POST end Figure 2 8 Definition of Thread connect 2 4 3 4 Camelot Compiler Test Report Up to now although Camelot has been used in a wide range most implementations 31 Chapter 2 of it are small and aim for particular problems The implementation of this project faces to a variety of problems Thus it is a good opportunity to test and improve the Came
43. cle for Proof Carrying Code like project Grail is required to 12 be the target for the Camelot compiler serve as a basis for attaching resource assertions be amenable to formal proof about resource usage provide a uniform format for sending and receiving guaranteed code be executable Chapter 1 Grail has two semantics one functional and one imperative both of which have direct connections with responsibilities listed above Grail s compiler is a part of Camelot s compiler so sometimes for simplification we can directly get a Java bytecode from a Camelot program using the compiler of Camelot 1 3 2 2 Space aware Type System Camelot in combination with its space type system enables to produce JVM bytecode endowed with guaranteed and certified bounds on heap space consumption MRG uses Hofmann Aspinall type system which provides an abstract type denoted lt gt as well as enforcing linear typing This abstract type called Diamond represents regions of heap allocated memory The motivation of designing a special diamond type is to allow better control of heap usage All non primitive types in a Camelot program are compiled to JVM objects of a single class Diamond which contains appropriate fields to hold data for a single node of any datatype Diamond values can be obtained through constructors for datatypes or released through match rules with special annotations Considering that there will be times that one m
44. clear the column in the normal manner Step 6 Go to step 3 All the entries on the last row are positive so we can get the solution now which is u01 0 u02 0 x01 0 y01 0 s01 0 s02 0 Z 0 Put the values to their proper position in the structure hd x01 list_1 u01 int u02 gt int y01 Then we can get the result hd 0 list_1 O int 0 gt int 0 which is the same as the one Ifd_infer computes 3 4 2 Experiment Problem Report And Analysis Since the whole Camelot code is quite large for convenience we separate them into several parts based on datatypes they operate on and then carry out the experiment on each of these parts During this period some problems have been notified by lfd_infer but after analysis we find out that most of them result from shortcomings of lfd_infer itself Next we will describe and analyze these problems Problem 1 LP For the Whole Program is Infeasible Reason Misuse of Destructive Pattern Match This problem happens when Ifd_ infer tries to solve stringpairlist cmlt which collects all functions on the datatype stringpairlist and stringintlist cmlt which collects all functions on the datatype stringintlist Actual implementation can be 53 Chapter 3 found in Appendix F Take stringpairlist cmlt for example we finally discovered that the problem is ascribed to the function let showStringPairList l stringpairlist k int n int sink string string if
45. code to the code consumer together with a proof produced by the proof producer which indicates that this code abides by the safety policy Y The code consumer checks whether the proof is valid for the code and the safety policy v Ifthe proof passes the check the code then can be executed on the code consumer side Proof Producer NN mw Figure 1 1 Overview of Proof Carrying Code Chapter 1 The principle of Proof Carrying Code is to construct and verify a mathematical proof about the machine language program itself and this guarantees safety but only if there s no bug in the verification condition generator or in the logical axioms or typing rules or the proof checker 11 As 12 points out a major advantage of this approach is that it sidesteps the difficult issue of trust there is no need to trust either the code producer or a centralized certification authority If some code comes with a proof that it does not violate a certain security property and the proof can be verified then it does not matter who wrote this code the property is guaranteed to hold But the user does need to trust certain elements of the infrastructure the code that checks the proof the soundness of the logical system in which the proof is expressed and of course the correctness of the implementation of the virtual machine that runs the code however these components are fixed and so can be checked once and for all Compared with 1
46. contain a claim of resource usage together with a proof of the claim 12 The proof expressed in a program logic for Grail follows a custom logic of partial correctness Sequents are of the form pe P which means that a Grail expression eeexpr is related to a specification P under some set of assumptions I of the same form The specification P denotes a predicate which can constrain possible executions of e with respect to the dynamic semantic 42 Chapter 3 pointed out above Specifications can refer to the initial and final heaps of a program expression the initial environment the resources consumed and the result value 25 The uniform judgement in the program logic is Fe AEhh vp PEhh vp which means that whenever the execution of e for initial heap h and environment E terminated and delivers final heap h result v and resources p P is satisfied that is that EF h e hy p implies P E h h v p Figure 3 4 shows the concrete rules of this logic As we will see besides rules for each form of Grail expression e expr two basic rules are provided as well e P eT VAX T gt e P VEhh vp PEhh vp gt QEhh vp VCONSE Tee P Tepe P Q VNULL I gt null AEhhvp h hav null a p 10 0 0 ec VINT Tpinti AEhhvp h hav inp l 00 0 VVAR T gt var x AEhh vp h hav E x a p 1 00 0 VPRIM T gt prim op x y AEhh vp v op E x E y ah ha p 3 00 0 VGETF gt xt AEhh vp Al x Re
47. ction enables the designer to incorporate system specific remedial action such as transfer to manual control shutting down of non critical tasks or other actions Second grow the stack or heap segment after it is out of memory into previously un utilized space such as dead variables and space freed by compressed live variables This technique can avoid the out of memory error if the extra space recovered is enough to complete execution 1 Surpassing the hardware method this method achieves space recovery and memory protection with low system overheads 1 2 Proof Carrying Code Proof Carrying Code PCC provides an alternative method for achieving memory safety The same idea can be applied to other safety properties covering data access policies resource usage bounds and data abstraction boundaries 8 Chapter 1 What is Proof Carrying Code Proof Carrying Code as pioneered by Necula and Lee 9 10 is a general framework for verifying the safety properties of machine language programs 11 PCC enables a computer system to determine automatically and with certainty that program code provided by another system is safe to install and execute without interpretation or run time checking 8 The key ideas behind PCC involve five concepts code producer code consumer proof producer safety policy and proof which are VY The code consumer requests code from the code producer specifying a safety policy Vv The code producer sends
48. d that considering in Java any method with object return type may return the null object Camelot provides a construct isnull e which tests if the expression e is a null value However in the previous compiler 32 Chapter 2 this construct has not been implemented yet 7 Released the constraint that variable names had to begin with lower case letters This improvement tones with some programmers habits that they get used to have classes names begin with upper case letters 8 Enabled the compiler to work on Windows system There was a problem in the previous compiler where the compiler couldn t recognize filenames with colons in them like E WTK22 lib so at that time in Windows the compiler could not recognize the name of the file which includes the Java classes we need 33 Chapter 3 Chapter 3 Inference of Heap Space Bounds The Goal of the Mobile Resource Guarantees MRG project is to develop Proof Carrying Code PCC technology to endow mobile code with certificate of bounded resource consumption These certificates are generated by a compiler actually the combined compiler for Camelot and Grail which in addition to translating high level programs into machine code derives formal proofs based on programmer annotations and program analysis 22 Programmer annotations enable programmers to express and manage storage allocation explicitly The program analysis takes space reuse by explicit deallocation into acc
49. dix D Appendix D 2 Actions in The Game This game allows actions Observe observe the current room s information Use use personal objects points of some parameters can be increased Take Room Object take an object from the current room Take Room Weapon take an weapon from the current room Talk talk to a player inside the same room Fight fight with a player inside the same room Change Room leave the current room and enter another room Check My Weapons Check My Objects Check My Points check the player s information These actions can be divided into following three categories Self Actions Local amp Asynchronous Environmental Action Local amp Synchronous Interactive Action P2P amp Asynchronous Action Local P2P Synchronou Asynchronou s s To observe To use Personal obj To take Room Objects Room Weapons To Check My Objects My Weapons My Points To talk Players To fight Players To change room 75 Appendix D Appendix D 3 The Categories of Objects Objects of the game are divided into several categories based on the parameter they have effect on Category 1 Health Points Category 2 Strength Category 3 Agility Category 4 Cash Category 5 Health Points amp Strength Category 6 Strength amp Agility Category 7 Health amp Agility 76 Appendix D Appendix D 4 Self Defined Datatypes type objectlist Nil Cons of o
50. dow mobile code with certificate of bounded resource consumption These certifications contain a claim of resource usage together with a proof of the claim The proof is expressed in the program logic we mentioned in section 3 2 2 and the claim of resource usage can be obtained by the use of lfd_infer an implementation of static prediction of heap space usage for first order functional programs This project uses this tool to infer the heap consumption of pure Camelot codes in our game However Ifd_infer has its shortcomings which partly make effects on the accuracy of the result These shortcomings are Functional objects as allowed in Camelot are currently not accounted for Therefore we only perform inference on the Camelot code without objects The term memory leak is not accurate in lfd_infer We have to make some artificial things in order to pass the inference and these introduce the accuracy of the result about the heap usage Sometimes programmers are required to adjust objective functions created by Ifd_infer themselves so as to get reasonable solutions to their functions 67 Chapter 4 4 2 Further Work As for the further work not only on the game itself but also on the analysis on resource consumption of the game major suggestions are 1 Game Interface The user interface of the current game is quite simple For a game which hopes to attract its players the user interface is a critical part JEME provides
51. e entry in G the method body satisfies the specification for any arguments passed to the body via the formal parameters 25 also proves soundness and completeness of this program logic which establishes a solid and convincing basis for the usage of the logic 3 3 Inference of Heap Space Bounds The Diamond type in Camelot together with its resource aware type system allows the heap usage of Camelot programs to be inferred Next we use lIfd_ infer the practical implementation to understand the procedure of getting an inference for heap space usage 3 3 1 Introduction of Ifd_infer Ifd_infer is the implementation aiming for the static prediction of heap space usage for first order functional programs as proposed by M Hofmann and S Jost in 2003 The process of type inference first sets up a set of linear inequalities over the rational variables on the fly by reconstructing a typing derivation for a given program These equalities together with a rather arbitrary objective function form a linear program which is then fed to an external LP solver where an optimal solution for this linear programming problem is calculated Making use of the solution set an annotated typing for each of the program s functions is established as well as a linear bound on each function s heap space consumption Some major features of this implementation are 45 Chapter 3 1 All build in types are assumed to be unboxed i e heap free including the
52. e in Camelot enables in place operations and precise control of heap usage A freelist for the storage of unused diamonds is provided for the case where one may not always want to reuse a diamond value immediately Since a safe and static automation of the decision about whether a pattern match is destructive or not is not available it is our programmers responsibility to ensure that the datatype we are going to deconstruct will not be used anymore because its heap space will be reclaimed and its contents will be overwritten subsequently We have mentioned in the previous section that there are two kinds of destructive match patterns in Camelot one uses d annotation and the other uses _ For the inference implementation of the static prediction of heap space usage introduced in the next section both of them are treated as _ as this will not affect the inference in any way So it is not a big matter whether to use d or _ but it is a matter of distinguishing whether to use a destructive pattern match or a read only pattern match Following codes are the examples of their usage in this project type card NullCard Card of int string string int int int string let attAbility c match c with Weapon _ _ _ attak attak NullWeapon gt 0 Figure 2 6 a A Method in the Project Using Read Only Match let concatList Il cardpairlist L12 ardpairlist match Il with Nil6 gt Cons6 a b th d gt
53. e sum of per thread space allocation plus the space requirements of the threads themselves 20 49 Chapter 3 3 4 Practical Work on the Inference of Heap Space Bounds This section will use the lfd_ infer to analyze the heap space usage of our game program Since functional objects allowed in Camelot are currently not yet accounted for in lfd infer so we have to pick out some pure Camelot code and deploy the experiment on them 3 4 1 Verifying Correctness of the Inference Result The Camelot code named simple cmlt is quite simple let hd 1 match with gt 0 h _ gt h The inference result of the heap consumption is hd 0 list_1 O int 0 gt int 0 which means that hd is a function taking as argument an integer list and return an integer after computation There is no extra heap cell required excepts for those originally allocated to hold the input list Figure 5 shows all generated constraints which are used for inference 50 Chapter 3 This file is an automatically generated lp for Ip_ solve simple constraints Contains 4 inequalties in 6 variables ie hd x01 list_1 u01 int u02 gt int y01 r MIN 4 u01 4 u02 2 x01 1 y01 hd _11_Val l a02 1 y01 lt 0 hd __11_M 2 1 a02 1 u02 1 x01 lt 0 hd__10 Val 1 a01 1 y0Ol lt 0 hd 10 M l 1 a01 1 u01l 1 x01 lt 0 a01 gt 0 a02 gt 0 u0l gt 0 u02 gt 0 x0l gt 0 yOl gt 0 a01
54. en ssElementAt t k 1 else Pair2 a b let sizeof l stringpairlist match with Nil4 gt 0 Cons4 a b t gt 1 sizeof t let rmPlayer l stringpairlist pname string stringpairlist match with Nil4 Nil4 Cons4 a b t gt if a pname then t else rmPlayer t pname let findNumber l stringpairlist pname string string match with Nil4 gt Cons4 a b t gt if a pname then b else findNumber t pname let copyStringPairList ll stringpairlist 12 stringpairlist match l1 with Nil4 12 Cons4 a b t gt let 12 Cons4 a b 12 in copyStringPairList t 12 79 Appendix E let showStringPairList l stringpairlist k int n int sink string string if k lt n then begin match ssElementAt k with Pair2 key value gt let snk sink player key phone in showStringPairList k 1 n sink None2 gt sink value n end else sink let getValue l stringpairlist key string match with Nil4 gt Cons4 a b t gt if a key then b else getValue t key let stringAt l stringlist k int match with Nil5 gt Cons5 h t gt if k gt 0 then stringAt t k 1 else h let clearStringPairList l stringpairlist match with Nil4 gt Cons4 a b t _ gt clearStringPairList t stringintlist cmlt type string intlist Nil3 Cons3 of string int string intlist type string int pair Nonel P
55. ent usage in Camelot is given in figure 2 2 type intlist Nil Cons int intlist let copylist ll intlist I2 intlist match I1 with Nil gt 12 Cons h t gt let 12 Cons h 12 in copylist t 12 Figure 2 2 Example for Match Statement in Camelot Chapter 2 6 Camelot also allows self defined datatypes but with a requirement that datatype constructors must begin with an upper case letter 7 string type in Camelot is immutable different from the one in OCaml where the ith element of a string type variable s can be obtained through s i 8 In OCaml we use arr i to retrieve the ith element of an array arr but in Camelot we use the built in function for array get arr i Besides for this Camelot still has several other functions on arrays like empty int gt a gt a array set a array gt int gt unit and arraylength a array gt int 9 OCaml provides an append operator on lists but Camelot reserves this symbol for use with rules of the diamond type which is a special type for explicit resource allocation 10 Camelot does not have the operator in OCaml in Camelot can be applied to strings and other objects However it is interpreted as equality of references and hence will usually fail to give the expected result for strings we should use the function same_string 22 11 Functions in Camelot are defined using the keyword Jet rather than fun or function which are used in OCaml
56. er 2 class roomgame javax microedition midlet MIDlet with field connM connectionManager field ui userInterface field mrecv message Receiver Constructor of the class maker let ui lt new userInterface this in let _ connM lt new connectionManager this in Signals the MIDlet that it has entered the Active state method startApp unit let this ui startMenu inlet _ this connM openMessageListener in end Figure 2 7 the Room Class in the Project 3 Concurrent Programming Thread is a frequently used concept in this project As we can see connect which is responsible for the communication between the peer and the server messageSender which is responsible for sending messages to other peers messageReceiver which is responsible for listening and receiving messages from other peers and room which is responsible for operations on the room i e update the object weapon list enqueue the incoming request for the Token process query about a specific object weapon in the room and so on The common ground of them is when they are doing their jobs the game is still going on without interruption Camelot provides two kinds of forms for thread declarations One is the standard form used for class declarations and the other are derived forms we mentioned in section 2 3 3 Derived forms for thread creation and use in Camelot contain a Java method java lang Thread setDaemon of
57. flAh hav h ta p 2 000 LV PUTE T gt x t y AEhh vpAl E x Ref la p 3 00 O A x s h h lt gt E y Avel VGETST T gt cOt AEhhvp h hav h c ta p 2 00 0 a VPUTST TecOt AEhhvp h i So SIRE e000 43 Chapter 3 VNEW Tp new cl 1 x AEhh vp All freshloc h A p n 1 0 0 0 Ah h efi E x av Refl Peeck T gt e P T gt ifx then e else e AEhhvp3p p p 2 00 O A E x true gt PEhhyp A VIF E x false gt P Ehhvp E x truev E x false Peezh T gt e P I gt letx e ine AEhhvp3p p hw PEhhwp Aw L P E x w hhvp p 1000 8 p Up VLET Pee ck T gt e P T gt e e AEhhvpAp p h PEhh L p A PEhh vp p p V Pr VCOMP TU call f P gt snd FT f AEhhvp PEhhy 1 1 0 0 p r gt callf P VCALL rU com a P gt snd MT c m AEhh vp VE E newframe null fst MT c m a E PE hhiv 2 a 01 1 p Tr gt cOm a P ee rU xm a P gt snd MT c m AEhhvp YE classOf E hx c E newframe E x fst MT c m a E gt E h hiv 4 a 01 1 p eP vvinv gt xem a P 44 Chapter 3 finite D D gt ee P GCD provable D G Gpe P goodContext MST G finite G c m y MST m y nut EG 0 gt c m z MST m z null VCUT VADAPTS Figure 3 4 The Program Logic for Grail The goodContext property requires that whenever a method invocation is associated to its specification tabl
58. gion set constraint inequality 1 objective function Figure 3 7 Changed Linear Problem 3 4 3 Heap Consumption of This Project Although our project implements a multi threaded game system constrained by the capability of the inference tool our experiment results are oriented to a single thread On the other hand no thread in our program uses those pure Camelot functions without operations on objects we mentioned here So for this project heap space usage of pure Camelot codes for one thread is equal to it for multi threads Next I will list the inference results of all the pure Camelot codes in this project which are separated by datatypes codes operate on 59 Chapter 3 stringpairlist clearStringPairList 0 stringpairlist 0 string string 0 stringpairlist 0 string string 0 0 copyStringPairList 0 stringpairlist 0 string string 1 stringpairlist 0 string string 0 stringpairlist 0 string string 0 0 findNumber 0 stringpairlist 0 string string 0 gt string string 0 getValue 0 stringpairlist 0 string string 0 gt string gt string 0 rmPlayer 0 stringpairlist 0 string string 0 string stringpairlist 0 string string 0 0 same _ string 0 string string gt bool 0 showStringPairList 1 stringpairlist 0 string string 0 int gt int gt string gt string 1 sizeof 0 stringpairlist 0 string st
59. gramming language which is a member of the ML family OCaml shares the functional and imperative features of ML but adds object oriented concepts and has minor syntax differences 18 Appendix A shows a relationship tree which indicates how ML was influenced by and has influenced other languages together with the development of ML You might get a general knowledge about the ML family there 2 1 1 The Core Language 2 1 1 1 The Basics of OCaml OCaml offers basic built in types bool int float char string as well as predefined data structures tuples lists and arrays In addition to these OCaml allows user defined data structures like records and variants In OCaml everything is an expression so everything returns a value Variables of OCaml are immutable that is once they are bound to a value they cannot be changed except by a new fresh binding While this seems very limiting to a programmer who is accustomed to other programming styles it enforces safe programming by not allowing side effects Functions in OCaml are values that are bound to names and treated as first class values Strictly speaking no function in OCaml takes more than one argument Multiple argument functions are actually curried functions OCaml enables conditional computation which is performed with the traditional if then else construct OCaml is not a pure function language It has looping constructs like while and for Chapter 2 loops as well as mut
60. gure 3 3 with judgements in the form EFH h eU hy p meaning that in variable environment E and initial heap h code e evaluates to the value v yielding the heap h and consuming p resources 25 Here resources refers to a tuple of four counters p clock calle invke invkdpth Representation of these four components is shown in table 3 2 The operational semantics and the program logic employ two operators on resources p q and p U q For their effects on the resources components refer to table 3 3 NULL INT E Fh null h null 1 0 0 0 Eth inti h i 1 0 0 0 Eth var x h E x 1 0 0 0 ae E Fh prim op x y h op E x E y 3 0 0 0 Do E x Ref E Fh xt A h t 2 0 0 0 GETF Refl heap reference of location 1 E x Ref1 Eth xt yU h lth E y 1 3 00 0 PUTF E Fh cOt U h h c t 2 0 0 0 ee E hcOt y h ct E y L 3 00 0 PFST l freshloc h Eth new c t x al b ofi E x Ref L 000 NEW freshloc h returns a fresh location outside the domain of h 40 Chapter 3 E x true Eth e y h v p IFTRUE Eth if x then e else e h v 2 0 0 0 p E x false Et h e y h v p EFh ifx then e else e U h v 2 0 0 0 p IFFALSE EFh e y hw p WAL E x w Fhe y h v q LET EFh letx e ine L h v 1 0 0 0 poq oy Ethe V h 1 p Eth e h v q EFh e e U h v
61. hd thena 1 else hd insert a tl Figure 2 1 a insertion sort in ocaml let insertal match with gt a hd tl _7 gt if a lt hd thena hd tl else hd insert a tl let sort 1 match l with gt hd tl _ insert hd sort tl Figure 2 1 b In place Insertion Sort in Camelot Chapter 2 let insertal match with gt a hd tlh d gt if a lt hd thena hd tl h d else hd insert a tl d let sort match l with gt hd tl d gt insert hd sort tl d Figure 2 1 c Another In place Insertion Sort in Camelot Figure 2 1 Insertion Sort 2 OCaml supports higher order functions but Camelot does not In Camelot any invocation of a function must supply exactly the same number of arguments as are specified in the definition of the function 3 Iterative constructs are not available in Camelot Camelot only supports recursive definitions or invocations 4 Camelot does not support exception signaling and handling as well as the module notion 5 Camelot also uses the match statement for datatype deconstruction but the form of it is much more restricted than the one of OCaml 21 This means that there must be exactly one rule for each constructor in the associated datatype and each rule binds the values contained in the constructor to variables or discards them by using the pseudo variable _ 21 An example of match statem
62. he other hand as a kind of embedded systems programming a mobile device is very different from programming a general purpose workstation Developers face problems such as conserving the battery life which have no analogue in traditional desktop computing One of the most significant costs of battery energy in mobile devices is memory usage For this reason developers benefit from using programming languages which give precise guarantees of resource consumption that can be inferred directly from the application code Camelot is just this sort of programming language which in combination with its space aware type system provides quantitative guarantees about the consumption of resources such as memory usage 1 4 2 Principle Goal of the Project The principle goal of this case study project is developing an on line game application in the Camelot programming language which would be compiled to run on an emulator for a Java enabled mobile phone most implementations of Camelot so far are small and aim for particular problems and the implementation of this project will face a variety of problems Thus it is a good opportunity to test and improve the Camelot compiler using an implementation of a static inference on heap space usage to get quantitative results about the consumption of the resource used by our game 1 4 3 Preparation for the Project Before carrying out this project some preparations have been made 11 Chapter 1
63. he total number of objects created and the maximum number in active use simultaneously 20 For the second problem although there is some way to place a bound on the heap space used by the new OO features within a Camelot program external Java code may use arbitrary amounts of heap With respect to this problem 29 proposes and analyzes three approaches The first is that only external classes which come with proofs of bounded heap usage are allowed to be used But constructing a resource bounded Java class library or inferring resource bounds for an existing library would be massive work even for the smaller class libraries used with mobile devices The second approach is to leave programmers or library creators to state the resource usage of the external methods they produce This requires extending the trusted computing base in the sense of resources but seems a more reasonable solution 29 The third is to only take account of resources consumed by Camelot code This suggestion seems somewhat unrealistic as one could easily cheat by using Java libraries to do some memory consuming dirty work 29 3 3 2 2 Heap Usage Problem Caused by Threads The analysis of memory consumption of Camelot programs is based on the consumption of memory by heap allocated data structures The present analysis of Camelot programs is based on a single threaded architecture To assist with the development of the thread management system in Camelot analysis
64. ies and corresponding effects are shown in Appendix D 3 Players have to explore rooms to collect as many points as possible to improve their personal parameters They might encounter obstacle in the special room or be attacked by other players On this occasion the winner can have his points increased and obtain an object from the loser At the same time the loser may lose some points or an object If one of the player s parameters reaches zero except for 23 Chapter 2 the health the player has to quit the current room and be transferred back to the start area of the current level But if the health reaches zero the player cannot play anymore The winner of this game is the one who can pass through all challenges successively reach the special room in the last level and pass the test there 2 3 2 Facilities There are several facilities required to establish as the basis of this project First from the point of location the game can be generally divided into two parts the server which is responsible for clients registration login information management and so on and the client where actual actions of the game occur So setting up a web server to carry out jobs on the server side is pre requisite for this project Second since this game is oriented to large numbers of players so a database is required to store all players information as well as to provide query service when necessary The third is a special package for mob
65. ile phone application development and the corresponding platform for testing Considering the cost and possibilities we finally choose Apache Tomcat as our servlet container postgreSQL as the underlying database management system Java API provided by J2ME as the special development package and KVM as the underlying design platform All of them are free and have large installed bases of users 2 3 3 Implementation in Detail 2 3 3 1 Architecture of the Game As a whole although the developed system involves a server and clients it actually follows a distributed architecture The meaning of this is that some services of the system are provided by the Network These kind of services are different from traditional client server ones because in client server architecture clients always know where to locate the service because the services is almost always at the same address but in a distributed environment like the one implemented in this case 24 Chapter 2 study the service moves from one location to another And the entity responsible for some service is a set of peers instead of a central entity the server Thus in order to locate a service peers must send messages to the Network to find out the information they need This system has a Peer to Peer nature which means that most communication happens between the players devices so the figure of the Server is limited only to administrative procedure 17 such as registration
66. is a kind of burden for them and is dangerous for programs A program might crash if a destructive pattern match is not the last access to that data Although there is an ongoing research aiming at this problem programmers currently still have to devote some attention on this problem when designing their programs 3 3 2 Further Discussion About Heap Space Usage 3 3 2 1 Heap Usage Problem Caused by Camelot s Object Oriented Feature As described earlier the presence of mutable objects in object oriented Camelot provides in place update 20 However by allowing arbitrary object creation the unbounded heap usage problem solved for datatypes recurs on this occasion Perhaps more seriously invocating arbitrary Java code in Camelot programs might lead to an unlimited heap space usage For the first problem the first attempt to directly adapt the idea of diamonds seems unrealistic since it is hardly appropriate to represent every Java object uniformly by 47 Chapter 3 an object of one class So an abstract diamond is proposed instead which represents the heap storage but used by an arbitrary object Any requirement is satisfied by using new to supply one of these diamonds But a problem of this approach is that reclamation of such abstract diamonds would only correspond to making an object available for garbage collection rather than definitely being able to re use the storage Even so such a system might be able to give a measure of t
67. ist 1 objectlist 0 obj 0 int string int int string 0 0 gt int gt int gt string gt string 1 copyObjectList 0 objectlist 0 obj 0 int string int int string 0 1 objectlist 0 obj 0 int string int int string 0 0 objectlist 0 obj 0 int string int int string 0 0 0 findObject 0 objectlist 0 obj 0 int string int int string 0 0 int gt int gt int gt obj 0 int string int int string O 0 objElementAt 1 objectlist 0 obj 0 int string int int string 0 0 int obj 0 int string int int string O 0 objectListLength 0 objectlist 0 obj 0 int string int int string 0 0 gt int 0 oid 0 obj 0 int string int int string 0 int 0 oname 0 obj 0 int string int int string 0 string 0 owner 0 obj 0 int string int int string 0 string 0 removeObject 0 objectlist 0 obj 0 int string int int string 0 0 int objectlist 0 obj 0 int string int int string O 0 0 showObjectList 0 objectlist 0 obj 0 int string int int string 0 0 int gt int gt string gt string 0 showSortedObject 0 objectlist 0 obj 0 int string int int string 0 0 gt int gt int gt string gt string 0 string of _int 0 int gt string 0 62 Chapter 3 cardlist attAbility 0 card 0 int string string int int int
68. k lt n then begin match ssElementAt l k with Pair2 key value gt let sink sink player key AA phone value n in showStringPairList l k 1 n sink None2 gt sink end else sink And this function further calls the function let ssElementAt l stringpairlist k match l with Nil4 gt None Cons4 a b t gt if k gt 0 then ssElementAt t k 1 else Pair2 a b which has LFD type ssElementAt 1 stringpairlist 0 string string 0 gt int stringstringpair 1 string string 0 0 This means that to execute function ssElementAt without running out of memory we need at least one free heap cell available before the function starts This is due to the possibility of executing the constructor Pair2 a b which needs a heap cell to hold the pair On the other hand since we don t know values of parameters n and k in advance it is impossible to decide how often showStringPairList calls ssElementAt and therefore how much memory showStringPairList will need This is the reason for LP being infeasible Furthermore instead of halting at this point Ifd_infer continues computing heap usage for the remaining functions so we still 54 Chapter 3 obtain an LFD type for showStringPairList even though it is wrong The LFD type below says that showStringPairList doesn t consume any memory but this is incorrect since we need some space to store the input list show String PairList 0 string
69. lds methods method methods field field x t field mutable x 7 val x 7 method maker x 7 X t super x exp method m x z x Tp T exp method m T exp let m x t x Tp T exp let m0 T exp Figure 2 3 The Syntax of a Class Definition in Camelot 20 Chapter 2 class cname Define a class called cname lt scname with gt Inherit from a class called scname implement iname Implement an interface called iname field lt mutable gt x t eG ee field named x of type t optionally be declared to be mutable valx T Static fields named x of type t maker x T1 Xn Tn naio of the class with arguments x of lt super Xj1 Xim gt exp type T Xn of type Tn the superclass maker is optionally executed and expression exp is executed method m x1 71 Xn 2 Tn T Instance method named m of type t with exp arguments x of type T Xn of type Tn expression exp is executed method m Tt exp Instance method named m of type t with xero argument expression exp is executed let m x1 T1 Xn Tn T EXP Static method named m of type with arguments x of type Ti Xn of type Tn let m T exp Static method named m of type t with xero expression exp is executed argument expression exp is executed Table 2 2 Explanation of items in the Class Definition Syntax 2 3 3 Extended With Concurrency In Camelot
70. lot compiler Followings are the improvements made to the compiler during this period All the fixing works on Camelot compiler were done by Dr Kenneth MacKenzie LFCS Univ of Edinburgh 1 Added new types byte long and so on for our need to access data like byte arrays For example storeMyInfo is a method in the connectionManager class which is responsible for telling the Server the current status of the player Since the output stream only accepts byte data so the player s information has to be changed to byte array first 2 Fixed a parsing problem In this project there are some contexts where we only can put long name like java microedition lcdui Alert but short class name like connectionManager are sometimes needed as well The previous Camelot compiler cannot recognize the short class name The solution to this problem perfects Camelot s OO features since now we not only can define our own classes but also can use them 3 Fixed the problem that the compiler sometimes failed to find methods which were defined in superclasses 4 Fixed the problem where the compiler confused the character type with the integer type and therefore it couldn t find the correct method 5 Originally datatypes weren t allowed to contain objects for example it was considered as a syntax error if we defined a type like type t A of java math BigInteger int 6 Added the isnull construct In 21 it is mentione
71. n the call to ssElementAt but is recovered when we do the destructive match and can be used again the next time we call ssElementAt When we eventually return from showStringPairList this heap cell will be free for other functions to use so we get the return type string 1 Moreover showStringPairList is the only function invoking ssElementAt So the overall consumption of these two functions is also equal to the size of inputs The third LFD type shown above is copyStringPairList 0 stringpairlist 0 string string 1 stringpairlist 0 string string 0 stringpairlist 0 string string 0 0 which means that executing copyStringPairList may allocate a number of extra heap cells equal to the length of the input list one free heap cell per Cons node of the input list So in this case the heap space consumption of the function is the double of the input list s length which includes the space to hold the input list at the very beginning 64 Chapter 3 Besides for what we have discussed above another heap space consumption is the heap space required for those codes involving objects In section 3 3 2 1 we have presented several solutions to this problem Here we point out again just because it also needs to be taken account of when we want to get an accurate result of the overall heap space consumption of the program Furthermore since different functions might be used in different circumstances which implies that
72. ng the Token has the right to access resources and perform the action he requested Other players must wait and their requests will be enqueued Programming a mobile device is very different from programming a general purpose workstation because of the resource limit on the former For this reason developers can benefit from using programming languages like Camelot to get precise guarantees of resource consumption which are inferred directly from the application code Camelot is an OCaml like functional programming language which compiles to a high level analogue of Java byte code named Grail Camelot is equipped with a mechanism which enables programmers have precise control on 66 Chapter 4 memory especially heap space usage Moreover although Camelot has been used in a wide range most implementations of it so far are small and aim for particular problems The implementation of this project faces to a set of various problems Thus it is a good opportunity to help test and improve the compiler of Camelot Some improvements have been made to the compiler during this period are Added new datatypes Fixed a parsing problem related to the class name in Camelot Fixed a problem caused by class inheritance Allowed datatypes contain objects Added the isnull construct Released the constraint on variable names Enabled the compiler to work on Windows system The Goal of the Mobile Resource Guarantees MRG project is to en
73. ot possible via the high level type system for example it may be possible to prove tighter resource bounds this way This experimentation work can be carried out using the Isabelle interactive theorem prover 69 Appendix A Appendix A ML Family Evolution Tree ERE POP Standard ML has also influenced following lanquaqes STANDARD ML moc SI ad a W A Eg m O oo STANDARD URGH eel ML suo perro STANDARD CONCURRE NT Appendix B Appendix B The Syntax of Camelot The terms tycoon con fname and var refer to type constructors constructors function names and variable names respectively The term tyvar refers to a type variable which is a name beginning with a single quote program typedecseq valdecseq funimplseq typedecseq typedec typedecseq type sec type ty var ty var tycon conbind conbind con of Oi or 2 conbind con conbind ty int char bool float string unit byte long tycar ty array tyseq tycon Ty ty Ty gt Ty gt ty higer order type valdecseq valdec valdecseq valdec val var ty val fname Ty funimplseq funimpl funimplseq funimpl ee let rec fundecseq 71 Appendix B fundecseq fundec and fundecseq fundec fname varseq expr expr const var fname fname expr expr if expr then expr else expr let pat expr in expr match expr with match
74. ount and also furnishes an upper bound on the heap usage in the presence of garbage collection 23 The program analysis relies on the type system which makes reference to the above programmer annotations Linear Programming LP is used to automatically infer derivations in this enriched type system 23 Following this line this chapter first gives a literature review about linear programming the program logic that connects with the outcome of space inference and the core inference for heap space usage After that analysis of the practical inference work on our program will be given as well 3 1 Linear Programming A linear programming problem is one in which we are to find the maximum or minimum value of a linear expression ax by cy called the objective function subject to a number of linear constraints of the form Ax By Cy t lt 5N or Ax By Cy 2 N called linear inequality 34 Chapter 3 The largest or smallest value of the objective function is called the optimal value and a collection of values of x y z that gives the optimal value constitutes an optimal solution The variables x y z are called the decision variables And the feasible region determined by a collection of linear inequalities is the collection of points that satisfy all of the inequalities Use of the graphic method gives you a more straightforward comprehension of this problem and its solution set For instance minimize Z 3x
75. p Space Bounds ccsscccsssccccsscccsssescessescesseseeees 34 3 1 Linear POST AMINO 2 otsccc ths bes ote tctantuga cteab liege dda than tant aeetetiauecsl Leas Cathlas 34 DOs Fhe Programi WOO 1G tas tice ts Sita aero clatter teat aialaegel At scenes aa 37 3 2 1 The Syntax and Operational Semantics of Grail eee eee 38 3 2 2 The Program Logic aii dese cscs Slaves yadeae peace tias sane ceom atiecennens 42 3 3 Inference of Heap Space Bounds xcs oisis elacedinelateds oho aad 45 3 3 1 Introduction of WG titers cicis5s aftasettecvmadatia ewan 45 3 3 2 Further Discussion About Heap Space Usage cecceeseeteees 47 3 4 Practical Work on the Inference of Heap Space Bounds e 50 3 4 1 Verifying Correctness of the Inference Result eee 50 3 4 2 Experiment Problem Report And Analysis cccesceesseeeteee 53 3 4 3 Heap Consumption of This Project ccceessceeseceeeeeeeeeneeeeeeees 59 Chapter 4 Conclusio sos sicsicsshdeskssatisnsdevevsneesncsaucavecdovsesetenncsvcensavesncsdauasdegatedecuacess 66 4 1 Project Summary cS hate ha eM Sa Sa a a Rael a eecht 66 4 2 Further Work corric ncenieisenrio naaid Aisles Ae eed Mes 68 Appendix A ML Family Evolution Tree cccsscccssscccssscsscssescessescessesceees 70 Appendix B The Syntax of Camelot eossoossoesssesssecssoossooesssesssesssoossoosssossssesssee 71 Appendix C Camelot s Built in Funtions esesooesooessoesssesssee
76. pairlist 0 string string 0 int int string string 0 The solution to this problem is to append _ to the pair constructor in showStringPairList as follows since we don t need the pair returned by ssElementAt again we can throw it away match ssElementAt l k with Pair2 key value _ gt As a result the program becomes feasible and corresponding correct LFD types are ssElementAt 1 stringpairlist 0 string string 0 int stringstringpair 1 string string 0 0 showStringPairList 1 stringpairlist 0 string string 0 int int string gt string 1 The type for showStringPairList says that it needs at least one free heap cell before it starts and leaves at least one free heap cell when it returns This heap cell is used up in the call to ssElementAt but is recovered when the destructive match is performed And again this heap cell is used the next time that ssElementAt is invoked When we eventually return from showStringPairList this heap cell will be reclaimed to the freelist for later use by other functions so we get the return type string 1 Problem 2 Memory Leak Reason Ifd_infer In the lfd_infer manual 28 memory leak problem is explained as the loss of references to heap cells Actually Ifd_infer s judgement for this problem is not accurate Our code is a proof of this Following is a function in 55 Chapter 3 objectlist cmlt Appendix F let clearObjec
77. ring 0 int 0 ssElementAt 1 stringpairlist 0 string string 0 int gt stringstringpair string string 0 0 stringAt 0 stringlist 0 string 0 int gt string 0 60 Chapter 3 stringintlist clearStringIntList 0 string int list 0 string int 0 string int list 0 string int 0 0 concatStringIntList 1 string int list 0 string int 0 int gt int gt string gt string 1 copyStringIntList 0 string int list 0 string int 1 string int list 0 string int 0 string int list 0 string int 0 0 findRoom 0 string intlist O string int 0 string int 0 lengthof 0 string intlist 0 string int 0 int 0 removeFirst 0 string int list 0 string int 0 string int list 0 string int 0 0 same _ string 0 string string bool 0 showStringIntList 1 string int list 0 string int 0 int gt int gt string string 1 siElementAt 1 string intlist 0 string int 0 int string int pair 1 string int 0 0 string _of _int 0 int gt string 0 61 Chapter 3 objectilist ability 0 obj O int string int int string 0 int 0 category 0 obj 0 int string int int string 0 int 0 clearObjectList 0 objectlist 0 obj 0 int string int int string 0 0 objectlist 0 obj 0 int string int int string 0 0 0 concatObjectL
78. s approach to achieving memory safety Proof Carrying Code has the potential to free the host system designer from relying on run time checking as the sole means of ensuring safety Authors of 8 further argue that by being limited to memory protection and run time checking for achieving memory safety designers of that kind of systems must impose substantial restrictions on the structure and implementation of the entire system Moreover Proof Carrying Code provides greater flexibility for designers of both the host system and then agents and also allows safety policies to be used that are more abstract and fine grained Chapter 1 than memory protection 8 1 3 MRG Project Mobile Resource Guarantees MRG is a European Commission funded project belonging to the Laboratory for Foundations of Computer Science MRG applied ideas from Proof Carrying Code to the problem of resource certification for mobile code 12 The aim of the project was to develop the infrastructure needed to endow mobile code with independently verifiable certificates describing its resource behaviour in the form of condensed and formalized mathematical proofs of resource related properties which are by their very nature self evident unforgeable and independent of trust networks 13 1 3 1 Architecture of MRG Code Producer Code Consumer Proof Checker W fi Camelot Code Resource Policy Runs code Figure 1 2 The Architecture of MRG
79. ssoossoossosssssessseee 73 Appendix D 1 The Map of The Game ssesssesssessseessoossooesssesssesssocssoossoossssesssee 74 Appendix D 2 Actions in The Game ssssssesssesssoossoossoosssoesssesssoossoosssosssoesssese 75 Appendix D 3 The Categories of Objects ssessseeesoceesoossssesssesssooesoosssossssesssee 76 Appendix D 4 Self Defined Datatypes e ssesssecssoossooessosssoesssesssoossoossosssssesssese 77 Appendix D 5 E R Diagram Of the Database scssscssssssssessssssscsssenees 78 Appendix E Pure Camelot Code in the Game eeessoessoeessesssocssoossoossssesssesssoee 79 Bibliography aeicsiinndesh osuascnds caedsissaisennsansiinsossns cececsuoueds ovacexsducbarteas eiucasassnseas esatecascecinsee 87 1 1 1 2 2 1 22 2 3 2 4 2 5 2 6 Dal 2 8 3 1 3 2 33 3 4 3 5 3 6 3 7 List of Figures Overview of Proof Carrying Code sssssssssereessssssssrrrrrrereesssssse 4 The Architecture Of MRG ne ccc ucaceiaclagsttaetarurcanieniacccseeds tceehaid 6 Insertion SOLE neeese kanscammnnpan E EE AEE EEEE seen keane unnmiaeaeant ree 17 Example for Match Statement in Camelot cceceeeeeeeeeee enone enone 17 The Syntax of a Class Definition in Camelot ccc eee eee ee eeneenee 20 Derived Forms for Thread Creation and use in Camelot 0064 22 Layered Arehitectute modani EE E A A E EEEE 25 Using The Diamond Type ssssssseeesnereesssssseserrrreeses
80. ssssseresesse 29 the Room Class in the Projets sica5csselawccirs vaprvictedaeehwiallawedare vaesivheeeeeetans 30 Definition of Thread connect sx sirosis even eases 31 Feasible Region for LP Program sesirsncaiard raecel ances cdelioncesinanteuneesa 35 Phe Syntax OF Grail sreo rinasr u nE a ET NAESER 38 The Dynamic Semantics of Grail 00 cece ccc ece ence nee e eens eee eneenne ees 41 The Program Logic for Grail cncssaccyesdace cae saveacassaensevedacatatiqedienseas 51 simple constraints All constraints for Inference eceeeeee ee eee eees 51 An Unbounded Case in Linear Programming ccceeeeeeeee eee es 58 Changed Linear Problemi s icctascarcecknciesdawa anene mashes AE Et 59 vi 2 1 2 2 2 3 3 1 3 2 3 3 3 4 List of Tables Basic Features of Camelot s Object System c ccc cceec cece eee eee 19 Explanation of items in the Class Definition Syntax 0 0 ceeceseeseeseeereeeees 21 Explanation of the Game Architecture ccceccec eee eneeeeee ene eneenens 26 Explanation of Grail s Syitax soccicjucsanas nas xypedansasdvnenraradanihteweannam vane 39 Representation of Resource s Four Components ceceeeee ener eens 42 Operations on ReSO rCE ce or e e EA EE E ET E ai 42 Solutions for the Heap Usage Problem of Multi Threads 5 49 vii Chapter 1 Chapter 1 Introduction 1 1 Embedded System Development Nowadays computing
81. st k match with Nil NullObject Cons h t gt if k gt 0 then objElementAt t k 1 else h let objectListLength l objectlist match with Nil gt 0 Cons h t gt 1 objectListLength t let clearObjectList l objectlist match with Nil gt Nil Cons h t gt clearObjectList t 84 Appendix E let removeObject l objectlist id int objectlist match with Nil gt Nil Cons h t _ gt if oid h id then let _ clearObject h in t else Cons h removeObject t id let findObject l objectlist id int k int n int obj if k lt n then let objxt objElementAt l k in if id oid objxt then objxt else findObject l id k 1 n else let objxt NullObject in objxt let concatObjectList l objectlist k int n int sink string ifk lt n then let objxtIns objElementAt l k in let snk sink string _of _int oid objxtiIns oname objxtins string _ of _int category objxtins string _of _int ability objxtins in concatObjectList k 1 n sink else sink let copyObjectList Il objectlist 12 objectlist match Il with Nil gt 12 Cons a t gt let 12 Cons a 12 in copyObjectList t 12 85 Appendix E let showSortedObject l objectlist k int n int sink string ifk lt n then let objxtIns objElementAt k inlet sink sink OBJECTS gt oname objxtIns category gt
82. string type This is not a bug although strings indeed use up heap space The reason for that is in most cases the use of strings is merely providing a convenient way for screen printing If heap space consumption of strings is a concern they can be treated as lists of characters or alternatively be restricted to a predefined length 2 For compatibility with Camelot Ifd_infer distinguishes a destructive from a read only pattern match The syntax is as match x with Cons a b c gt Read only match Cons a b c _ gt Destructive match cell goes to freelist Cons a b c d gt Destructive match cell bound to d of type lt gt Cons a b c Allocate heapcell from freelist Cons a b c _ Allocate heapcell from freelist Cons a b c d Use heapcell bound to d Of course there is only one match operation is allowed for each constructor among the above possibilities Furthermore in this system a node of a data structure on the heap can only be destroyed and built anew but it cannot be updated 3 lfd_infer allows programmers to enforce some annotations as they see fit This can be done using the enriched or annotated typing facility that it provides 4 Since modularity is inherent to the inference Ifd_infer supports partial inference 28 Any function which is defined but not declared i e there is no val statement corresponding to it will be ignored in the inference
83. string _of _int category objxtIns ability gt string _of _ int ability objxtins AN n n in showSortedObject l k 1 n sink else sink let showObjectList l objectlist k int n int sink ifk lt n then begin string string let objxtIns objElementAt l k in let sink sink oname objxtIns category gt string _of _int category objxtins Ability gt string _of _int ability objxtIns n in showObjectList k 1 n sink end else sink A 86 Bibliography Bibliography 1 Surupa Biswas Matthew Simpson Rajeev Barua Memory Overflow Protection for Embedded Systems using Run time Checks Reuse and Compression CASES 04 280 291 September 22 25 2004 2 Wind River High Availability Design for Embedded Systems Http www windriver com whitepapers high availability design html 3 George V Neville Neil Programming Without A Net ACM Queue Tomorrow s Computing Today 1 2 16 23 April 2003 4 Motorola M68000 User s Manual Prentice Hall Englewood Cliffs NJ 5 Intel i960Sx 32 bit Microprocessor Intel Corporation http www intel com design i960 documentation docs_sx htm 6 MSP430 Ultra Low Power MSUs Texas Instruments 2004 http focus ti com lit ml slab034g slab034 pdf 7 Michael Durrant Running Linux on low cost low power MMU less processors August 2000 http www linuxdevices com articles AT6245686197 html
84. systems are everywhere When we talk about them most of us think of desktop computers for example PC s laptops mainframes servers etc But there is another far more common type the embedded system An embedded system is a combination of computer hardware and software either fixed in capability or programmable for a specific computational task Compared with conventional desktop systems embedded systems consist of fairly standard components such as processors memory units buses peripherals as well as real time I O devices e g sensors and actuators In addition to these embedded systems also have their own characteristics Single functioned which means each of them execute a single program repeatedly Tightly constrained including low cost low power small fast etc Continually react to changes in the system s environment Must compute certain results in real time without delay Embedded systems are already used in a broad area from industrial machines automobiles medical equipment airplanes to toys vending machines as well as cell phones 1 1 1 Memory Overflow Concern Out of memory error is a serious problem in computing which becomes more critical in the context of the embedded system because of its limited memory and particular storage organization 1 points out that desktop systems can reduce the Chapter 1 ill effects of the out of memory problem through their virtual memories in two w
85. tList L objectlist match with Nil gt Nil Cons h t _ gt clearObjectList t Ifd_infer gives a LFD type clearObjectList 0 objectlist 0 obj u07 int string int int string u08 0 unit 0 and then prints a message warning of a the memory leak with an inequality clearObjectList 163 Ma2 1xK1 1xa69 1xu06 1xx03 lt 0 which means that the memory leak occurs in the branch of a destructive pattern match on the second constructor of the matched type We can see in this branch there is a reference for a heap cell represented by 1xK1 in the inequality released due to the destructive match Since there is not a datatype constructor from that point Ifd_infer falsely assumes that the heap cell pointed to by the released reference has been lost and therefore warns that a memory leak occurs In fact there is no leak clearObjectList works properly The heap cell released by the destructive pattern has been reclaimed and put in the free list recall the definition of _ If we give a list of length n as input there will be n extra heap cells put on the free list when clearObjectList returns The essential reason is that the LFD type system is not strong enough to express this Since clearObjectList returns a unit type the only possible return types for the function are things like unit 0 unit 1 unit n n21 Values appearing in LFD types have to be constants and the best the LFD type system can is to say that the
86. their inputs might vary so it s not possible for us in current condition to give an exact number of heap cells we require for our program One of the solutions to it is that we can impose more constraints on the inputs of some functions to make possible that we can expect which function will have what kind of input and how large of the input In this case providing an accurate result of heap space consumption becomes possible This idea also suggests a possibility of our future work 65 Chapter 4 Chapter 4 Conclusion 4 1 Project Summary This is a case study project of developing an on line game application in the Camelot programming language which has been compiled to run on an emulator for a Java enabled mobile phone Three major issues have been considered in the implementation The system deploys a distributed architecture Some services of the system are provided by the Network So peers in a virtual wireless environment need to broadcast their queries to locate the service they require The system is highly mobile and has a P2P nature Room is the most important mobile object of the system Copies of it move from one peer to another peer This move is actually a clone action which is achieved through the direct Peer to Peer communication The system provides environment actions which are local and synchronous Room is the critical section each of which has a Token for exclusive actions on it Only the player owni
87. tot WIR G cinco iti My eeipcadeedsn n a eusan eee 6 1 3 2 Components Of MRG scoits sre cssieece ea sake Sages ai nee 7 1 4 Desenipronor thesProject Atrcatuucaseescadenesatecatustceceuss oy Mareces tdactelacarea ties 10 1 4 1 Motivation and Description of the Project ceeeeseeeseeeteeeees 10 1 4 2 Principle Goal of the Project c8 cississisbeisctek eaiiedatinawiisinaues 11 1 4 3 Preparation for the Projpecty scueciattascecsescdintatisinstaisemeaniats 11 TS Struct re OF th Dissertaties Rec tat tay oh ae hes ot laut ace ah 12 Chapter 2 Camelot and the Case Stud y sccccsscccssscccssscsccsscsssssescesssssssesceees 13 2A OCaml Objective Camlas trousa oroia aaa alent Ta REE lage 13 2 1 1 TheCore Wan Cua oe ig sss28ccy htecnest dad iactusensieriactesbdeieedacdetaraeaeaesds 13 2 1 2 Object Oriented Features of OCaml cecceeeeeceeseeeteeeteeeees 14 22r Camelot st tage ac atta oe at al end haa OE aan dae ad 15 2 2 1 The Core Language Comparison between Camelot and OCaml 15 2 2 2 OCamelot Object Oriented Camelot cececceesseeesseeeteeeteeeees 18 2 3 3 Extended With Concurrency 4 4 ccnacasiwaaeheantansedsenet 21 2 3 Case Study Functional Embedded Telephony in Camelot 23 23A Game Storyline soisin oi ia aah A e E 23 23 2 Facilities oneiiearnianodrenni eee Waa and ew a Aas 24 2 3 3 Implementation in Detar lis case acuediviihn s caeedes ace oes eateries 24 Chapter 3 Inference of Hea
88. urce Aware Functional Language In Trends in Functional Programing Intellect Vol 4 pages 47 62 2004 91

2.3 Case Study: Functional Embedded Telephony in Camelot

Contents

Download Pdf Manuals

Related Search

Related Contents