![\includegraphics[scale=0.5]{MonashCrest.eps}](img1.png)
In building component-based systems, prediction and measurement of extra-functional properties of components have been elusive goals (Schmidt; 2001). Extra-functional execution properties such as performance (time), re-usability, reliability, availability, security, and responsiveness have not received much attention in terms of building executable specifications. These properties generally influence the cost-of-service of large-scale software systems. Specification of such extra-functional properties, and the impact on implementation of the executable specifications has not, as yet, been explored in great detail. While ASMs and AsmL address the basic, behavioural and synchronisation properties of a software specification, they do not address the above-mentioned quantitative extra-functional properties (Barnett and Schulte; 2001b).
The cost-of-service incurred due to extra-functional properties could be estimated to a certain extent by introducing tracking variables in executable specifications. Variables that track extra-functional properties could be specified, and measured during execution of the specification. Similar cost-of-service tracking variables could also be introduced in the implementation of the specification. Such a COST measure could help to bridge the gap between ASMs, AsmL and extra-functional properties, and at the same time lead to cost reduction of software development.
It should be noted however, that measuring the executable specification cost and measuring the actual implementation cost have entirely different meanings. The execution-time of the specification can be expected to be much worse compared to that of the implementation. For example, measuring and predicting time as an extra-functional property via executable specifications could therefore mean performing a symbolic calculation. Such a calculation would be made in terms of some justifiable time calculus calculated alongside the symbolic execution of the specification. These calculations will become a reference model and can be recorded in a similar way to the computation outcomes recorded for correctness proofs and checks. A testing approach would be taken when comparing the measured implementation costs (execution-time in this case) to those of the reference model. If the actual implementation measures disagree with the modeled properties, such violations can then be pinpointed so that the responsible parts (such as components or functions) of the system can be identified.
What is it that we study in computer science? What is computation? What are the peculiar dynamic systems of computer science? Thinking about these questions, I arrived at the notion of abstract state machine (ASM) as a formalization of the notion of computer system at any given level of abstraction.
Decomposing a computer system into a hierarchy of abstraction levels composed of states and operations was the initial purpose of Abstract State Machines. Since its inception, the concept has been the subject of various researches in different application domains including finite model theory, complexity theory and applied computer science (Börger; 2000).
Let A be any computer system at a fixed level of abstraction. There is an abstract state machine B that step-for-step simulates A.
The dynamic nature of a computer system is due to the fact that it has a state that evolves in time (Gurevich; 2001). An abstract state of a system is the representation of a system's state at any given instant. The evolution of a system from one state to the next is achieved by applying update rules to the current state of the system. The transition from one state to the next is called a step. The complete evolution of a system, from a starting point to the point where no more changes occur, is called a run.
A very simple example of an ASM model would be to consider a sorting machine that sorts an array using a single-swap algorithm like bubble sort or quick sort. For an unsorted array 
, where 
is the array value at index 
, sort can be defined as:
choose x,y in indices(A) such that x < y and A(x) > A(y)
do
A(x) := A(y)
A(y) := A(x)
The value of at each step is the state of the machine. The rule warrants the selection of any two indices, and 
, that satisfy the given conditions, 
and 
. This is followed by the swapping of array values at the chosen indices. The sorting ASM executes until no further updates are possible. No further updates are possible when the array is sorted (Modeled Computation LLC; 2001).
A diagrammatic representation of such a run would be:
Initially, the ASM thesis was used to solve problems related to the dynamics of programming languages. Egon Börger tried out the ASM approach to model the dynamics of PROLOG (Börger; 1990b; Börger; 1990a). The ASM approach led to ISO standardisation of the language. This was followed by the application of ASMs for specification and verification of machine architectures and protocols. The abstract and operational nature of ASMs led to its rapid success in developing executable specifications (Börger; 2000). The use of evolving algebras, and later ASMs, in hardware and software engineering, particularly for high level analysis and design was further investigated by Egon Börger (Börger; 1995,1999).
ASMs were used at Siemens Corporate Technology to design a railway process model named FALKO (Börger et al.; 2000). Barnett et al. (2000) discuss the use of ASMs at Microsoft by providing a relevant case study. A noted product group within Microsoft that uses ASM technology is the Universal Plug and Play group (Foundations of Software Engineering; 2003a; Glässer et al.; 2001). The last decade has seen ASMs being used primarily to develop executable specifications for complex software systems.
The .NET framework is built around the idea of the Common Language Runtime (CLR), which accepts code written in different languages and converts it to executables in the .NET framework. The CLR is an execution environment that promotes interoperability between different languages by means of a rich object-oriented class library. .NET software components are distributed in the Microsoft Intermediate Language (IL), which is executed by the CLR (Gordon and Syme; 2001). All .NET aware languages are compiled into IL, but are then re-compiled into native binary machine code at execution time. The Common Type System (CTS) of the .NET platform describes all possible types supported by the CLR, and their representation in the .NET metadata format. Languages that use the Common Language Subset (CLS), a subset of the CTS, are called .NET aware languages.
Model-based specification is an approach to formal specification where the system specification is expressed as a system state model. This state model is constructed using well-understood mathematical entities such as sets and functions. System operations are specified by defining how they affect the state of the system model.
Specifications are descriptions of how software components are supposed to work once they are implemented. Executable specifications add to the notion of traditional model-specifications by having a single and unambiguous meaning (Modeled Computation LLC for Microsoft; 2002a).
The AsmL specification language can be used to specify COM components and interfaces. AsmL also uses the CLS, thereby ensuring that contracts written using AsmL can be used seamlessly across all .NET aware languages (Barnett and Schulte; 2002). Microsoft currently uses AsmL for modelling, rapid prototyping, analysing, checking of APIs, devices, and protocols (Barnett and Schulte; 2001a).
Extra-functional issues have been approached in two ways in the past: process-oriented and product-oriented ways (Landes and Studer; 1995; Mylopoulos et al.; 1992). A product-oriented approach deals with extra-functionality at component level. Components come together with a description of services provided, and the signatures of the methods that provide the services. However, the specifications provided with components often lack information regarding interactions beyond interface compatibility. As a consequence, the extent of prediction and verification of system properties get restricted (Vieira et al.; 2001).
The extra-functional characteristics of software components are not always as apparent as functional properties. This often results in specifications that have not taken into account extra-functional issues. Such a specification becomes unbalanced and can lead to unexpected maintenance costs due to flawed design. Changes in system environment that occur during maintenance often modify the extra-functional conditions. These changes can also have a direct influence on the cost of maintenance as the extra-functional situations now need to be reviewed in light of the new system conditions (Franch and Botella; 1997).
The ability to reason about system properties based on the external abstractions of components would give specification developers a new added advantage. In this regard, Issarny et al. (1997) put forward the idea of QoS (Quality of Service) relating to extra-functional execution properties such as availability, security and responsiveness that depend largely on the processing environment. Lau (2001) talks about the difference between a posteriori and a priori reasoning and why the latter is more important and relevant when it comes to specifying software systems. Lau (2001) opines that ``pre- and post- conditions (with only proof-theoretic semantics) are not enough for specifying interfaces. Rather, we need declarative (e.g. model-theoretic) semantics''. Some work has also been done to predict system dependencies in component access points (Vieira et al.; 2001).
Schmidt and Zimmermann (1994) proposed different cost annotations for Object-Oriented (OO) Machines and applied them to OO Programs written in the Sather language. These authors also introduced a prediction calculus that is based on specific cost annotation measures. Such annotations are embedded in pre- and postconditions as Cost variables which keep track of the desired extra-functional properties. The primary aim of such abstract annotations were to provide a good basis for traditional software metrics. OO Machines, have a basis of algebra and are closely related to ASMs. This makes it possible to carry the cost annotations forward to a similar ASM model, something that has not yet been done.
It was decided that counter variables will be associated with methods to keep track of different cost-of-service attributes. Every method has its own space and time complexity information. Counters enable the developer to estimate the number of times a method will be called in a correct and practical implementation of the specification. These factors can be scaled from a method perspective to a high-level object perspective. If such a mechanism can be put in place for all methods, a realistic prediction about the cost-of-service of a software specification can be gained. For example, `space' complexity can be tracked on a method level by counting memory allocation, `time' can be tracked by counting execution cycles, and `throughput' can be tracked by counting transactions per unit time of an object.
We propose three types of counters with the following syntax for the case studies to be conducted as part of this research project:
![\includegraphics[scale=0.7]{asm02.eps}](img10.png)
NReq_methodname - Counts the number of requests for a method.
NBeg_methodname - Counts the number of started executions of a method.
NEnd_methodname - Counts the number of finished executions of a method.
The `N' at the beginning is an abbreviation for `number of'. This is followed by the type of counter: `Req' for request, `Beg' for begin and `End' for end counters respectively. In all the above cases, the `methodname' is replaced by the actual name of the method. Counters should be declared and initialised for methods that will be used frequently and can be thought of as having a considerable impact on the cost-of-service. These counters can also be used to establish class invariants. For example, a stack-based program cannot have more requests made to the pop function compared to the push function.
To introduce counters as cost-of-service tracking variables in executable specifications, we create a counter interface definition called ICounter in AsmL as shown in figure 5.1.
The declaration and initialisation of counter variables for methods are made easier with the introduction of the counter interface. Each method would have counter object(s) declared by means of this AsmL interface. The interface methods can also be used to increase, decrease and retrieve the value of a counter object. Object-oriented standards of AsmL.NET are maintained in the process. Dealing with counters as a cost-of-service tracking measure becomes easier as a result.
![\includegraphics[scale=0.8]{ICounter.eps}](img11.png)
CounterValue() method returns the current value of the counter variable associated with the caller object method. The Increment() method increments the object method counter by one and the Decrement() method decrements it by one. The simplicity of the Counter class makes it very easy to understand and use as a cost-of-service tracking measure. The Counter class is implemented in AsmL as shown in figure 5.2.
For the purpose of this research project, it was decided that counters would be used as a cost-of-service tracking measure on separate case studies. AsmL model specifications would be written and then refined to concrete implementations. The presence of counters in the specification and execution models would provide us with a measure of cost-of-service. We aimed to use cost-of-service measures introduced in specification models from the implementation to express a consistent cost measure. If the cost-of-service results tracked during specification-time execution were found to be similar to the results tracked during implementation-time execution, then the application of counters as a cost-of-service tracking measure would be proved successful. The feasibility of this approach could then be analysed, and further extended and scaled for larger and complex software solutions. The next chapter discusses the case-studies that were undertaken as part of this research project.
It was initially decided that counters will be introduced into the examples that accompany the AsmL for Microsoft .NET distribution as case studies for this project. This would let us build on the existing example specifications, instead of having to elicit requirements and specifications for a new problem. Based on the assumption that the provided example specifications are optimised in every possible way, introducing the aspect of cost-of-service into these specifications for the purpose of this research project would help in analysing results without having to take usual optimising factors such as efficiency and appropriateness of the specification into account. Out of the many provided examples, the `Stack' model was chosen as the first case study. The `Dining Philosophers' solution was extended to include counters as the second case-study. Lastly, a solution to the `Readers and Writers' problem, dependent on counters as an assertion measure to implement synchronisation, was developed.
![\includegraphics[scale=0.8]{CCounter.eps}](img12.png)
Push, Pop and Top. The state of the stack model is contained in a variable that is declared as a sequence of integers. We extend the stack specification provided as an example with the AsmL for Microsoft .NET distribution (Foundations of Software Engineering; 2003c) to a stack interface called IStack. The stack interface is then implemented as the Stack class where all the methods are defined. Stack objects are then instantiated to write a Reverse Polish Notation Calculator executable specification in AsmL.
Push(), Pop() and Top() methods are also declared, and the corresponding pre-requisites defined. The Push() method takes in an integer as an argument, and pushes that integer onto the stack. The Pop() method pops the topmost element from the stack. To pop an element from the top of the stack, there needs to be at least one or more elements in the stack. This pre-condition of the Pop() method is declared in the IStack interface. The Top() method returns the value of the topmost integer in the stack, without popping it off the stack. Similar to the Pop() method, this method also requires the state of the stack to be non-empty. A pre-condition to this end is declared in the IStack interface.
Three counter objects are declared for the Push(), Pop() and Top() methods. Due to the simple and sequential nature of a stack object, only `end' counters that are responsible for keeping track of finished executions of the relevant methods are declared. As detailed in section 5.1, the names of the method follow the type of counter that is being declared. The number of elements popped off a stack cannot be greater than the number of elements pushed onto the stack. This invariant can be confirmed by declaring an interface constraint that depends on counters. We establish the invariant by making sure that the `end' counter of the Push() method is always greater or equal to the end counter of the Pop() method. The code inside the boxes in figure 6.1 indicate the declaration of counters and the interface constraint in AsmL.
![\includegraphics[scale=0.8]{IStack.eps}](img13.png)
Push() method of a stack is responsible for pushing an element onto the top of the stack. In this case study, an additional step is added to the specification of a Push() method. After pushing the current element onto the stack, the `end' counter is incremented before execution of the method is completed. Similarly, after popping an integer from the stack, the `end' counter of the Pop() method is incremented before execution of the method is completed and control returns back to the caller. The Top() method returns the topmost element of the stack to the caller. Hence the `end' counter of this method is incremented before control is returned back to the caller. Although associating a counter with the Top() method might initially be akin to a futile exercise, careful and clever use of this counter can provide interesting measures as is illustrated in the Reverse Polish Notation Calculator implementation. Figure 6.2 shows the Stack class written in AsmL.
This RPN calculator specification written in AsmL iterates nine times, and exits after the user has been given the chance to perform nine operations on the stack elements. Since the stack is initialised to have ten elements, more than nine mathematical operations performed on the stack would lead to assertion violations. Before stopping execution, the program displays all the counter values that have been measured during execution. Detailed source code listing of the Reverse Polish Notation Calculator specification written in AsmL can be found in appendix A.1.
A stack object was instantiated to implement the RPN Calculator as mentioned in section 6.1.3. Figure 6.4 is a post-initialisation screen-shot of the Stack-based RPN Calculator written in AsmL as a case study for this research project. Ten integers between 1 and 100 have been pushed onto the stack, and the program is waiting for user input.
The program accepts nine user inputs, as the stack is initialised to have ten integer elements. Figure 6.5 is a screen-shot of a sample execution of the program that accepts user inputs and produces corresponding outputs. It is observed from this execution that the operations defined in the Stack and the Calc class work as expected. The counters are incremented at the end of each member method execution, thereby enforcing the interface invariant for the IStack interface. It is also noted that the number of executions of Push() is greater than the number of executions of Pop().
From the above observations, we can infer that the counter variables associated with each method provide a frequency measure of the method in question, and hence can be used as a cost-of-service tracking measure on a large-scale. Nine mathematical operations on a RPN Calculator executes the Push() method 16 times, and the Pop() method 15 times. Similar data retrieved during specification-time execution can provide an estimation of the resources likely to be used by a method during the course of a program execution. Such estimations can also be scaled to provide similar estimates for actual implementations of the specification in question.
![\includegraphics[scale=0.9]{CStack.eps}](img14.png)
![\includegraphics[]{stackRun.eps}](img15.png)
![\includegraphics[]{rpn01.eps}](img16.png)
![\includegraphics[scale=0.7]{rpn02.eps}](img17.png)
move() and canMove(). We add request, begin and end counters for the move() and canMove() methods to the abstract definition of a philosopher class. A displayCounters() method is also added to monitor the values of the counters after each move executed by the philosopher.
The implementation has five philosophers vying for five forks when their respective status is `Hungry'. A philosopher loops through the following states: Thinking, Hungry, HungryWithLeftFork and Eating. A philosopher requires both the forks to his/her left and right to commence eating. A structure called Fork is declared to denote a solitary fork, and a Set of forks is declared for the philosophers. Two methods left() and right() return the index of the corresponding forks of a philosopher. A philosopher has no forks while his/her current status is `Thinking'. A thinking philosopher becomes hungry and tries to procure the left fork, followed by the right fork. A philosopher can attain the `Eating' status only if both forks have been acquired. After eating for a while, the philosopher goes back to the `Thinking' state. Figure 6.6 shows the abstract Philosopher class written in AsmL.
A Table class is defined that controls the philosophers, and interacts with the external interface created in C#. A Table has a Set of Philosophers and a Map data structure to store relations between a Fork and a Philosopher. This class defines a Move() method, which acts as a global entry point to the AsmL specification from external implementations, such as the C# interface described later. The Move() method chooses a philosopher that can change state and executes a move() operation on that philosopher.
We introduce request, begin and end counters for the Move() method to track the number of times the philosophers are moved by a Table object, and also to track the number of external accesses performed on this AsmL specification. The Move() method also has a variable stepNo that is incremented after each execution of a philosopher move. Although the stepNo variable serves similar purposes as the counter variables, we retain this variable in our specification to perform comparisons with the counters that are introduced. Figure 6.7 shows a section of the Table class written in AsmL. The code inside the boxes indicate the initialised counters and their application as a COST measure.
The counter variables are declared for the different key methods as mentioned earlier, and are incremented as and when required in the AsmL specification. Globally accessible methods that return the values of the counters in the Table class as string variables are also defined. This is to facilitate access to the counters from the external C# interface. We introduce COST counters only to the `greedy' philosophers solution provided in the example, and do not retain the `generous' solution due to the limited scope of this research project. A full code listing of the dining philosophers specification written in AsmL for the purpose of this research project can be found in appendix B.1.
A square with a `P' denotes a `Thinking' philosopher in figure 6.8. Small squares marked with an `F' indicate forks in the interface as shown in figure 6.9. A square marked with a `P', and that has only one fork attached to it indicates a `Hungry' philosopher. If a square marked with `P' has both left and right forks attached to it, then that philosopher is currently in the `Eating' state. Clicking on the `Display Counters' button populates the text-box on the right hand side of the window as seen in figures 6.8 and 6.9. Before a `Move' or a `Run' is executed, all the counters associated with the Table class have the value zero as illustrated in 6.8.
Clicking on the `Move' button executes the Move() method of the Table object, which in turn moves a philosopher that is ready to move and change its state in the life-cycle. A sequence of these moves constitute a run. Each move made by a philosopher is tracked by the associated counter variable, and is displayed in the console by the AsmL specification as seen in figure 6.9. A deadlock situation is reached when each philosopher has acquired one fork and is waiting for the next fork. The `greedy' nature of this solution ensures that a philosopher does not release a fork before he/she has finished eating. Hence the possibility of a deadlock remains. Figure 6.9 illustrates a deadlock situation. The console displays the number of moves executed by each philosopher so far, and the `Dining Philosophers' window displays the counter values associated with the Table object.
As illustrated in figure 6.9, Philosopher 1 has made 137 moves, Philosopher 2 has made 149 moves, Philosopher 3 has made 113 moves, Philosopher 4 has made 121 moves, and Philosopher 5 has made 113 moves before the program has reached a deadlock state. Individual moves of philosophers add up to a total of 633, whereas the total number of moves the Table object tried to initiate were 638. The Move() method in figure 6.7 indicates a choose statement that is evaluated as part of each execution. A philosopher that is in a position to change his/her current state is chosen as part of this evaluation. The above observation where the total moves executed by philosophers is 633, and the total number of moves initiated by the Table object is 638 affirms the non-deterministic nature of the Move() method.
It can be observed from this case-study that integrating external components written in .NET aware languages, with classes written in AsmL, is not extremely difficult. The fact that counters used as cost-of-service tracking measures in AsmL specifications can be easily used and extended as part of a concrete implementation is also illustrated. It is also observed that counters can be used to track the number of times a globally accessible method is accessed by external components. The value displayed after `Step #' on the top left hand section of the `Dining Philosophers' window, and the `Move() Counter Values' as displayed on the text-box on the right hand side of figure 6.9 are the same. This demonstrates that cost-of-service tracking variables can replace existing variables that are sparsely introduced for counting purposes.
Using Counter objects as described in section 5.3 helps to commit other tracking in a consistent manner, as well as using them for COST. Similar to the previous case-study, we observe again that association of counter variables with each method provides a frequency measure during requirements elicitation and specification generation. These measures can be scaled to provide realistic estimates for large scale software systems during design and implementation.
![\includegraphics[]{philo01.eps}](img18.png)
![\includegraphics[]{philoTable.eps}](img19.png)
![\includegraphics[scale=0.8]{dp01.eps}](img20.png)
![\includegraphics[scale=0.8]{dp04.eps}](img21.png)
Read() and Write() methods. The variable numberOfReaders in the Reader class keeps track of the number of readers that are in execution at a given instant. The difference between NBeg_Read and NEnd_Read gives us the number of readers currently in execution. The UpdateReaders() method is called after every counter increment or decrement to update the numberOfReaders variable. The Readers() method returns the numberOfReaders to the caller. The value of the NEnd_Read counter tells us the number of successful read operations that have been executed so far. The TotalReaders() method returns this value to the caller. Figure 6.10 shows the Reader class written in AsmL.
The Writer class has corresponding methods similar to the Reader class for the above-mentioned purposes. Since we develop a solution where waiting writers are given preference over waiting readers, we define a WritersWaiting() method. The difference between the number of requests made to the Write() method, and the number of started executions of the Write() method gives us the number of writers that are waiting to access the shared resource. The WritersWaiting() method calculates the number of waiting writers and returns the value to the caller. Figure 6.11 shows the Writer class written in AsmL. Detailed source code listing of the Reader and Writer classes can be found in appendix C.1.
The BeginRead() method verifies if any writer threads are in execution and whether there are any threads waiting to write to the shared resource. The Writers() method and the WritersWaiting() method in the AsmL specification are used by the BeginRead() method for this purpose. The current thread waits for the writers to signal after they finish execution. We have similar begin and end methods for writers that wait and signal as appropriate by evaluating pre-conditions in terms of the COST counters defined in the AsmL specification. The total number of readers and writers that have finished execution are also incremented based on the COST counters. Figure 6.12 shows the user interface used to initialise and execute the threads, display the counters, and exit the program.
The interoperability between AsmL specifications and corresponding implementations is evident from this case study. The ease of introducing cost-of-service tracking measures is also demonstrated. An existing dynamic link library can be refined to include COST counters by merely adding a Counter class and defining a corresponding abstract class with appropriate counter objects. The synchronisation developed as part of this case study in the C# implementation using COST counters defined in the AsmL specification also establishes the fact that assertions defined in an AsmL specification can be easily translated and used in a corresponding implementation. Figure 6.14 is a screen-shot of the program execution after the threads have performed random read and write operations on a shared resource, and have now stopped. The `Number of Reads' and the `Number of Writes' are displayed by the C# implementation, but the values are retrieved from the appropriate COST counters that are defined in the AsmL specification.
From the observations made during this case study, we accentuate the theory that extra-functional properties can be tracked with considerable ease by introducing COST counters in an AsmL specification, and by using them in equivalent correct implementations. The ability to count the total number of read and write operations performed by using counters also demonstrates the ability to create a trace of history by using COST counters. A history trace can be used to implement bounded conditions to stop or start required executions once a counter reaches a pre-defined threshold. The successful tracking implemented in this case study also establishes that COST counters can be specified in both sequential and parallel system specifications.
Once a class or a method has been tagged with a cost attribute, counters would be automatically declared and instantiated as required. In case of a class, all methods in the class will have counters that can be used for cost-of-service tracking. If it is desired that all methods of a class do not require associated COST counters barring one, then the individual method in question can be classified as a cost method.
The above mechanism should help in cost-of-service tracking of extra-functional, as well as functional properties in AsmL specifications, and can be further used in correct implementations written in any .NET aware programming language. The user is given full flexibility of tagging methods and classes that require tracking. It is a very simple and minimal proposal that can have far-reaching benefits in terms of reducing cost of software development, specially in the .NET environment. The object-oriented and abstraction properties of AsmL are also retained by using the counter interface and class. Specification of this proposal was out of the scope of this project, and can be an extensive undertaking for future projects.
This project adds a new dimension to ASM-based executable specifications by devising a way to track cost attributes of extra-functional properties in software systems. This opens up the prospect of specification, prediction and verification of extra-functional properties for large-scale software systems.
Estimation of extra-functional properties during specification using the developed cost-of-service tracking measure reduces costs in various direct and indirect ways. For example, a real-time system, where high-speed performance is desired, might be able to use the estimated information to add more hardware to the system in the design phase to improve performance, as opposed to doing the same during the implementation or testing phase. Similarly, estimating response time for desktop programs might help to attract more users, or prevent loss of users due to slow response time.
An abstract model based on the theory of Abstract State Machines was developed to track cost-of-service as part of this research project. A Counter class and interface were designed and implemented in the case studies that were conducted. The Abstract State Machine Language was used for the case studies. The observations made from the case studies prove the effectiveness of this approach as a tracking measure. Different ways of associating the counters with different extra-functional properties were also illustrated as part of the case studies. Interoperability of this solution with the .NET framework makes it a viable approach to optimise a .NET framework based software system for extra-functional properties during specification phase.
As illustrated in figure 7.1, comments beginning with //@ will be parsed and replaced with appropriate `Begin' and `End' methods that would declare and initialise counters for the method. Optional assertions can be inserted in the comments inside square brackets. These assertions will also be inserted in the `Begin' and `End' methods as required. Such pre-processing would help to introduce counters, and establish program-wide invariants and assertions in terms of the `Begin' and `End' methods generated by the pre-processor. After pre-processing the code example in figure 7.1, the source code input for the AsmL compiler would be as shown in 7.2.
Due to time-constraints and the complex nature of this undertaking, a basic pre-processor could not be developed as desired. Implementation of such a pre-processor can be done in future, and integrated with the .NET development environment. This is currently a work in progress, and can be further pursued as part of a PhD research project.
interface ICounter var counter as Integer = 0 CounterValue() as Integer Increment() Decrement()
![\includegraphics[scale=0.8]{reader.eps}](img22.png)
![\includegraphics[scale=0.8]{writer.eps}](img23.png)
![\includegraphics[scale=0.8]{rwWindow.eps}](img24.png)
![\includegraphics[]{rwExecTrace.eps}](img25.png)
![\includegraphics[]{rwEnd.eps}](img26.png)
![\includegraphics[scale=0.8]{cost.eps}](img27.png){kind=small}
![\includegraphics[]{precode.eps}](img28.png)
![\includegraphics[]{postcode.eps}](img29.png)
class Counter implements ICounter
CounterValue() as Integer
step
return counter
Increment()
step
counter := counter + 1
Decrement()
step
counter := counter - 1
interface IStack
// a stack of integers
var s as Seq of Integer = []
// Counter variables to count number of requests to 'push'es and 'pop's.
// 'begin' and 'end' counters are not introduced as this is a trivial
// example to illustrate the notion of counter variables.
var NEnd_push = new Counter()
var NEnd_pop = new Counter()
var NEnd_top = new Counter()
// Pushes an integer onto the stack
Push(i as Integer)
// Pops an integer from the stack
// Requires a non-empty stack
Pop()
require s <> []
// Returns the topmost member of the stack
// Requires a non-empty stack
Top() as Integer
require s <> []
// Displays the value of the counters
DisplayCounters()
constraint NEnd_push.CounterValue() >= NEnd_pop.CounterValue()
class Stack implements IStack
Push(i as Integer)
step
// pushes item onto the stack
step 1: s := [i] + s
// increases the 'end' counter
step 2: NEnd_push.Increment()
Pop()
step
// pops item from the stack
step 1: s := Tail(s)
// increases the 'end' counter
step 2: NEnd_pop.Increment()
Top() as Integer
step
// increases the 'request' counter
step 1: NEnd_top.Increment()
// returns topmost item from the stack
step 2: return Head(s)
DisplayCounters()
step
step 1: WriteLine("\n\t Number of calls to Push() : "
+ NEnd_push.CounterValue())
step 2: WriteLine("\t Number of calls to Pop() : "
+ NEnd_pop.CounterValue())
step 3: WriteLine("\t Number of calls to Top() : "
+ NEnd_top.CounterValue() + "\n")
interface ICalc
Calculate()
class Calc implements ICalc
Calculate()
// Instantiate a new Stack
var myStack = new Stack()
// Declare and initialise counters
var calcLoopCounter as Integer = 0
var pushLoopCounter as Integer = 0
// Declare and initialise current operator
var current as Char = ' '
// Declare and initialise arguments
var arg1 as Integer = 0
var arg2 as Integer = 0
var stackElement = 0
// Push 10 integers onto the Stack
// Uses non-determinism to a certain extent
step while pushLoopCounter < 10
step stackElement := any x | x in {0..100}
step myStack.Push(stackElement)
step WriteLine("Pushing ... Top element after Push(): "
+ myStack.Top())
step pushLoopCounter := pushLoopCounter + 1
step
WriteLine("\n" + myStack.s) // Prints out stack
// user input loop begins
// The 'AssertionFailed' exception can be raised by iterating
// the following loop 10 times (number of elements in the stack)
step while calcLoopCounter < 9
step WriteLine("\nEnter operator + - * / = or `ctrl+c' to quit")
step current := ReadLine() as Char
//step WriteLine(current)
step
if current = '+' then
step
step WriteLine("Stack : \t" + myStack.s)
step WriteLine("Operator : \t" + current)
step arg1 := myStack.Top()
step myStack.Pop()
step arg2 := myStack.Top()
step myStack.Pop()
step myStack.Push(arg1 + arg2)
step WriteLine("Stack : \t" + myStack.s + "\n")
else
(if current = '-' then
step
step WriteLine("Stack : \t" + myStack.s)
step WriteLine("Operator : \t" + current)
step arg1 := myStack.Top()
step myStack.Pop()
step arg2 := myStack.Top()
step myStack.Pop()
step myStack.Push(arg1 - arg2)
step WriteLine("Stack : \t" + myStack.s + "\n")
else
(if current = '*' then
step
step WriteLine("Stack : \t" + myStack.s)
step WriteLine("Operator : \t" + current)
step arg1 := myStack.Top()
step myStack.Pop()
step arg2 := myStack.Top()
step myStack.Pop()
step myStack.Push(arg1 * arg2)
step WriteLine("Stack : \t" + myStack.s + "\n")
else
(if current = '/' then
step
step WriteLine("Stack : \t" + myStack.s)
step WriteLine("Operator : \t" + current)
step arg1 := myStack.Top()
step myStack.Pop()
step arg2 := myStack.Top()
step myStack.Pop()
step myStack.Push(arg1 / arg2)
step WriteLine("Stack : \t" + myStack.s + "\n")
else
(if current = '=' then
step
step WriteLine("Stack : \t" + myStack.s)
step WriteLine("Operator : \t" + current)
step WriteLine("Result : \t" + myStack.Top())
step myStack.Pop()
step WriteLine("Stack : \t"+myStack.s+"\n")
else
step WriteLine("Invalid Input")
)
)
)
)
step calcLoopCounter := calcLoopCounter + 1
// Display counter values at the end of execution
step myStack.DisplayCounters()
[EntryPoint] Main() var myCalc = new Calc() myCalc.Calculate()
[EntryPoint]
Main()
// create stack
var myStack = new Stack()
if myStack.s = [] then
WriteLine("Stack is Empty\n")
else
WriteLine("Stack not Empty\n")
// Push integers onto the Stack
// convert this to a 'foreach' loop maybe
initially x = 1
step while x < 6
step myStack.Push(x)
step WriteLine("Pushing ... Top element after Push(): "
+ myStack.Top())
step x := x + 1
step
if myStack.s = [] then
WriteLine("\nStack is Empty\n")
else
WriteLine("\nStack not Empty\n")
// Pop integers from the Stack
step
initially y = 1
step while y < 6
step WriteLine("Top element before Pop(): "
+ myStack.Top() + " Popping ...")
step myStack.Pop()
step y := y + 1
step
if myStack.s = [] then
WriteLine("\nStack is Empty\n")
else
WriteLine("\nStack not Empty\n")
myStack.Counters()
// [Rupak Das] Modified Code // [/Rupak Das]
namespace DiningPhilosophers
// [Rupak Das]
interface ICounter
var counter as Integer = 0
CounterValue() as Integer
Increment()
Decrement()
class Counter implements ICounter
[EntryPoint]
CounterValue() as Integer
step
return counter
[EntryPoint]
Increment()
step
counter := counter + 1
[EntryPoint]
Decrement()
step
counter := counter + 1
// [/Rupak Das]
// Defines the different states of philosophers enum State Thinking Hungry HungryWithLeftFork Eating structure Fork index as Integer
// Abstract philosopher class abstract class Philosopher var status as State = Thinking index as Integer // [Rupak Das] var NReq_canMove = new Counter() var NBeg_canMove = new Counter() var NEnd_canMove = new Counter() var NReq_move = new Counter() var NBeg_move = new Counter() var NEnd_move = new Counter() // [/Rupak Das] abstract canMove(table as Table) as Boolean abstract move(table as Table) // [Rupak Das] abstract displayCounters() // [/Rupak Das]
numPhilosophers as Integer = 5
numForks as Integer = numPhilosophers
forks as Set of Fork = {Fork(i) | i in {1..numForks}}
// [Rupak Das]
var NReq_left = new Counter()
var NReq_right = new Counter()
// [/Rupak Das]
left(p as Philosopher) as Fork
// [Rupak Das]
// NReq_left.Increment()
// WriteLine("Calls to left() by Philosopher " + p.index +
// ": " + NReq_left.CounterValue())
// [/Rupak Das]
return Fork(p.index)
right(p as Philosopher) as Fork
// [Rupak Das]
// NReq_right.Increment()
// WriteLine("Calls to right() by Philosopher " + p.index +
// ": " + NReq_left.CounterValue())
// [/Rupak Das]
return Fork(p.index mod numPhilosophers + 1)
class Table
philosophers as Set of Philosopher
var holder as Map of Fork to Philosopher = { -> }
var fed as Set of Philosopher = {}
var stepNo as Integer = 0
// [Rupak Das]
var NReq_Move = new Counter()
var NBeg_Move = new Counter()
var NEnd_Move = new Counter()
// [/Rupak Das]
[EntryPoint]
Move()
// [Rupak Das]
NReq_Move.Increment()
NBeg_Move.Increment()
// [/Rupak Das]
choose phil in philosophers where phil.canMove(me)
phil.move(me)
stepNo := stepNo + 1
// [Rupak Das]
NEnd_Move.Increment()
// [/Rupak Das]
[EntryPoint]
shared InitGreedy() as Table
philosophers = { new GreedyPhilosopher(i) as Philosopher |
i in [1..numPhilosophers] }
return new Table(philosophers)
// [Rupak Das]
[EntryPoint]
displayReqCounters() as String
return NReq_Move.CounterValue().ToString()
[EntryPoint]
displayBegCounters() as String
return NBeg_Move.CounterValue().ToString()
[EntryPoint]
displayEndCounters() as String
return NEnd_Move.CounterValue().ToString()
// [/Rupak Das]
HoldsLeft(philIndex as Integer) as Boolean
return exists (i,p) in holder where p.index = philIndex
and left(p) = i
HoldsRight(philIndex as Integer) as Boolean
return exists (i,p) in holder where p.index = philIndex
and right(p) = i
IsFeeded(philIndex as Integer) as Boolean
return exists p in fed where p.index = philIndex
IsDeadlock() as Boolean
return forall p in philosophers holds not p.canMove(me)
IsGreedy() as Boolean
return exists p in philosophers where p is GreedyPhilosopher
StepNo() as Integer
return stepNo
class GreedyPhilosopher extends Philosopher
override move(table as Table)
// [Rupak Das]
NReq_move.Increment()
NBeg_move.Increment()
// [/Rupak Das]
match status
Thinking : status := Hungry
Hungry : if not (left(me) in table.holder)
table.holder(left(me)) := me as Philosopher
status := HungryWithLeftFork
HungryWithLeftFork
: if not (right(me) in table.holder)
table.holder(right(me)) := me as Philosopher
status := Eating
add me to table.fed
Eating : remove table.holder(left(me))
remove table.holder(right(me))
status := Thinking
// [Rupak Das]
NEnd_move.Increment()
displayCounters()
// [/Rupak Das]
override canMove(table as Table) as Boolean
// [Rupak Das]
NReq_canMove.Increment()
NBeg_canMove.Increment()
NEnd_canMove.Increment()
// [/Rupak Das]
return status = Thinking
or (status = Hungry and left(me) notin table.holder)
or (status = HungryWithLeftFork and right(me) notin table.holder)
or status = Eating
// [Rupak Das]
override displayCounters()
step WriteLine("Philosopher " + me.index + " has made "
+ NEnd_move.CounterValue() + " moves")
// [/Rupak Das]
// [Rupak Das] Modified Code // [/Rupak Das]
//
// Foundations of Software Engineering
// Microsoft Research
// (c) Microsoft Corporation. All rights reserved.
//
// Modified by Rupak Das for research purposes
// Dated: 20th October, 2003
//
using System;
using System.Drawing;
using System.Collections;
using System.ComponentModel;
using System.Windows.Forms;
namespace DiningPhilosophers
{
/// <summary>
/// Summary description for View.
/// </summary>
public class View : System.Windows.Forms.Form
{
private System.Windows.Forms.Label Phi1;
private System.Windows.Forms.Label Phi3;
private System.Windows.Forms.Label Phi2;
private System.Windows.Forms.Label Phi4;
private System.Windows.Forms.Label Phi5;
private System.Windows.Forms.Button Run;
private System.Windows.Forms.Button Quit;
private System.Windows.Forms.Label Counter;
private System.Windows.Forms.Label Fork1l;
private System.Windows.Forms.Label Fork1r;
private System.Windows.Forms.Label Fork2l;
private System.Windows.Forms.Label Fork2r;
private System.Windows.Forms.Label Fork3l;
private System.Windows.Forms.Label Fork3r;
private System.Windows.Forms.Label Fork4l;
private System.Windows.Forms.Label Fork4r;
private System.Windows.Forms.Label Fork5l;
private System.Windows.Forms.Label Fork5r;
private System.Windows.Forms.Button Greedy;
private System.Windows.Forms.Label[] Phils;
private System.Windows.Forms.Label[] Forks;
private System.Windows.Forms.Button Step;
private Table table;
// [Rupak Das]
private System.Windows.Forms.Button displayCounterBtn;
private System.Windows.Forms.TextBox counterTxt;
// [/Rupak Das]
/// <summary>
/// Required designer variable.
/// </summary>
private System.ComponentModel.Container components = null;
public View()
{
//
// Required for Windows Form Designer support
//
InitializeComponent();
Phils = new System.Windows.Forms.Label[]{Phi1,Phi2,Phi3,
Phi4,Phi5};
Forks = new System.Windows.Forms.Label[]{Fork1r,Fork1l,
Fork2r,Fork2l,
Fork3r,Fork3l,
Fork4r,Fork4l,
Fork5r,Fork5l};
Step.Click += new EventHandler(OnStep);
Run.Click += new EventHandler(OnRun);
Quit.Click += new EventHandler(OnQuit);
Greedy.Click += new EventHandler(OnGreedy);
// [Rupak Das]
// Generous.Click += new EventHandler(OnGenerous);
// [/Rupak Das]
table = Table.InitGreedy();
Redraw();
}
/// <summary>
/// Clean up any resources being used.
/// </summary>
protected override void Dispose( bool disposing )
{
if( disposing )
{
if(components != null)
{
components.Dispose();
}
}
base.Dispose( disposing );
}
// The windows form designer generated code
// was left out of this listing due to page-limit
// constraints.
#region Windows Form Designer generated code
#endregion
void Redraw()
{
for (int i = 1; i <= 5; i++)
{
Forks[(i-1)*2].Visible = table.HoldsLeft(i);
Forks[(i-1)*2+1].Visible = table.HoldsRight(i);
if (table.IsFeeded(i))
{
Phils[i-1].BackColor = Color.Green;
}
else
{
Phils[i-1].BackColor = Color.Yellow;
}
}
// [Rupak Das]
Counter.Text = (table.IsGreedy() ? "Step #" :
"generous step #") + table.StepNo()
+ (table.IsDeadlock() ? " results in deadlock." : "");
if(table.IsDeadlock())
{
Console.WriteLine("DeadLock");
}
// [/Rupak Das]
}
void OnStep(object o,System.EventArgs a)
{
table.Move();
Redraw();
}
void OnRun(object o,System.EventArgs a)
{
int max = 5000;
while (!table.IsDeadlock() && max-- > 0)
{
OnStep(o,a);
this.Update();
}
Redraw();
Counter.Text += ", stopping.";
Counter.Update();
}
void OnQuit(object o,System.EventArgs a)
{
Application.Exit();
}
void OnGreedy(object o,System.EventArgs a)
{
table = Table.InitGreedy();
Redraw();
}
// [Rupak Das]
/*void OnGenerous(object o,System.EventArgs a)
{
table = Table.InitGenerous();
Redraw();
}*/
// [/Rupak Das]
[STAThread]
static void Main()
{
Application.Run(new View());
}
// [Rupak Das]
private void displayCounterBtn_Click(object sender,
System.EventArgs e)
{
counterTxt.AppendText("\r\n\r\n");
counterTxt.AppendText(" NReq_Move: ");
counterTxt.Text += table.displayReqCounters();
counterTxt.Text += "\r\n NBeg_Move: ";
counterTxt.Text += table.displayBegCounters();
counterTxt.Text += "\r\n NEnd_Move: ";
counterTxt.Text += table.displayEndCounters();
}
// [/Rupak Das]
}
}
namespace ReaderWriter
interface ICounter
var counter as Integer = 0
CounterValue() as Integer
Increment()
Decrement()
class Counter implements ICounter
CounterValue() as Integer
step
return counter
Increment()
step
counter := counter + 1
Decrement()
step
counter := counter - 1
[EntryPoint]
public class Reader
var NReq_Read = new Counter()
var NBeg_Read = new Counter()
var NEnd_Read = new Counter()
var numberOfReaders as Integer = 0
[EntryPoint]
BegRead()
NReq_Read.Increment()
NBeg_Read.Increment()
UpdateReaders()
[EntryPoint]
Read()
BegRead()
// An actual read operation is not
// performed as the aim of this task
// was to implement synchronisation,
// and not performing file I/O
WriteLine("Reading ...")
EndRead()
[EntryPoint]
EndRead()
NEnd_Read.Increment()
UpdateReaders()
[EntryPoint]
UpdateReaders()
numberOfReaders = NBeg_Read.CounterValue()
- NEnd_Read.CounterValue()
[EntryPoint]
Readers() as Integer
step
return numberOfReaders
[EntryPoint]
TotalReaders() as Integer
step
return NEnd_Read.CounterValue()
[EntryPoint]
public class Writer
var NReq_Write = new Counter()
var NBeg_Write = new Counter()
var NEnd_Write = new Counter()
var numberOfWriters as Integer = 0
[EntryPoint]
BegWrite()
NReq_Write.Increment()
[EntryPoint]
Write()
NBeg_Write.Increment()
UpdateWriters()
// An actual write operation is not
// performed as the aim of this task
// was to implement synchronisation,
// and not performing file I/O
WriteLine("Writing ...")
EndWrite()
[EntryPoint]
EndWrite()
NEnd_Write.Increment()
UpdateWriters()
[EntryPoint]
UpdateWriters()
numberOfWriters = NBeg_Write.CounterValue()
- NEnd_Write.CounterValue()
[EntryPoint]
Writers() as Integer
step
return numberOfWriters
[EntryPoint]
WritersWaiting() as Integer
step
return NReq_Write.CounterValue()
- NBeg_Write.CounterValue()
[EntryPoint]
TotalWriters() as Integer
step
return NEnd_Write.CounterValue()
using System;
using System.Drawing;
using System.Collections;
using System.ComponentModel;
using System.Windows.Forms;
using System.Threading;
namespace ReaderWriter
{
/// <summary>
/// Summary description for ReadWrite.
/// </summary>
public class ReadWrite : System.Windows.Forms.Form
{
/// <summary>
/// Required designer variable.
/// </summary>
private System.ComponentModel.Container components = null;
Reader myReader = new Reader();
Writer myWriter = new Writer();
AutoResetEvent autoEvent = new AutoResetEvent(false);
const int numThreads = 26;
public static bool running = true;
private System.Windows.Forms.Button InitialiseBtn;
private System.Windows.Forms.TextBox statusBox;
private System.Windows.Forms.Button counterBtn;
private System.Windows.Forms.Label readLbl;
private System.Windows.Forms.Label writeLbl;
private System.Windows.Forms.Button exitBtn;
private static Random rnd = new Random();
private int totalReads = 0;
private int totalWrites = 0;
public ReadWrite()
{
//
// Required for Windows Form Designer support
//
InitializeComponent();
}
/// <summary>
/// Clean up any resources being used.
/// </summary>
protected override void Dispose( bool disposing )
{
if( disposing )
{
if(components != null)
{
components.Dispose();
}
}
base.Dispose( disposing );
}
// The windows form designer generated code
// was left out of this listing due to page-limit
// constraints.
#region Windows Form Designer generated code
#endregion
public void BeginRead()
{
try
{
// require Writers() eq 1 and WritersWaiting eq 0
while (myWriter.Writers() != 1 &&
myWriter.WritersWaiting() != 0)
{
Console.WriteLine("... Waiting to Read ...");
autoEvent.WaitOne();
}
myReader.Read();
Thread.Sleep(100);
//statusBox.Text += "\r\nReading ...";
EndRead();
}
catch
{
}
}
public void EndRead()
{
Console.WriteLine("Signalling Writers ...");
autoEvent.Set();
}
public void BeginWrite()
{
myWriter.BegWrite();
try
{
// require Readers() eq 0
while (myReader.Readers() != 0)
{
Console.WriteLine("... Waiting to Write ...");
autoEvent.WaitOne();
}
myWriter.Write();
Thread.Sleep(500);
//statusBox.Text += "\r\nWriting ...";
EndWrite();
}
catch
{}
}
public void EndWrite()
{
if (myWriter.WritersWaiting() == 0)
{
Console.WriteLine("Signalling Readers ...");
autoEvent.Set();
}
}
public void ThreadProc()
{
while (running)
{
double action = rnd.NextDouble();
if (action < 0.8)
{
//statusBox.Text += "\r\nReading ...";
BeginRead();
}
else
{
//statusBox.Text += "\r\nWriting ...";
BeginWrite();
}
}
}
private void InitialiseBtn_Click(object sender,
System.EventArgs e)
{
readLbl.Text = "Number of Reads:";
writeLbl.Text = "Number of Writes:";
// Start a series of threads.
// Each thread randomly performs reads and writes on
// shared resources.
statusBox.Text = "Status:\r\nInitialising ...";
Thread[] t = new Thread[numThreads];
for (int i = 0; i < numThreads; i++)
{
t[i] = new Thread(new ThreadStart(ThreadProc));
t[i].Name = new string(Convert.ToChar(i + 65), 1);
statusBox.Text += "\r\nStarting thread "
+ t[i].Name.ToString();
t[i].Start();
if (i > 10)
{
Thread.Sleep(1500);
}
}
// Shut down all threads
running = false;
for (int i = 0; i < numThreads; i++)
{
totalReads += myReader.TotalReaders();
totalWrites += myWriter.TotalWriters();
Console.WriteLine("Total Reads by Thread "
+ t[i].Name.ToString()
+ ":\t {0}", myReader.TotalReaders());
Console.WriteLine("Total Writes by Thread "
+ t[i].Name.ToString()
+ ":\t {0}", myWriter.TotalWriters());*/
//autoEvent.Set();
//t[i].Join();
t[i].Join(30);
}
Console.WriteLine("\r\n{0} reads and {1} writes executed.",
totalReads, totalWrites);
Console.WriteLine("THE END");
}
private void counterBtn_Click(object sender, System.EventArgs e)
{
readLbl.Text = "Number of Reads:\r\n" + totalReads;
writeLbl.Text = "Number of Writes:\r\n" + totalWrites;
}
[STAThread]
static void Main()
{
Application.Run(new ReadWrite());
}
private void exitBtn_Click(object sender, System.EventArgs e)
{
Application.Exit();
}
}
}
This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.48)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -dir html -t COST:Cost-of-Service thesis04Nov.tex
The translation was initiated by MR RUPAK DAS on 2003-11-13