A systematic incrementalization technique and its application to hardware design

A systematic transformation method based on incrementalization and value caching generalizes a broad family of program optimizations. It yields significant performance improvements in many program classes, including iterative schemes that characterize hardware specifications. CACHET is an interactive incrementalization tool. Although incrementalization is highly structured and automatable, better results are obtained through interaction, where the main task is to guide term rewriting based on data-specific identities. Incrementalization specialized to iteration corresponds to strength reduction, a familiar program improvement technique. This correspondence is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm, which has also served as an example of theorem prover-based implementation verification. Published online: 9 October 2001 RID="*" ID="*"S.D. Johnson supported, in part, by the National Science Foundation under grant MIP-9601358. RID="**" ID="**"Y.A. Liu supported in part by the National Science Foundation under grant CCR-9711253, the Office of Naval Research under grant N00014-99-1-0132, and Motorola Inc. under a Motorola University Partnership in Research Grant. RID="***" ID="***"Y. Zhang is a student recipient of a Motorola University Partnership in Research Grant.     

The PROSPER toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they can be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the software toolkit developed by the project. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit. Published online: 19 November 2002 Work funded by ESPRIT Framework IV Grant LTR 26241. RID="*" ID="*"Michael Norrish is supported by the Michael and Morven Heller Research Fellowship at St. Catharine’s College, Cambridge. RID="**" ID="**"Konrad Slind is now at the School of Computing, University of Utah, Salt Lake City UT 84112, USA.     

Consistent specification of interface suites in UML

The paper motivates and describes a model oriented approach for consistent specification of interface suites in UML. An interface suite is a coherent collection of interfaces defining interactions that transcend component boundaries. The specification of interface suites contains diagrammatic views and documentation, but it is extended with templates for structured specifications deriving from the ISpec approach. To guarantee that the specification views, documentation and templates are consistent, a specification model has been constructed. The model contains both structural and behavioural information, represented in the form of sequences of carefully designed tuples. The model provides the underlying structure for the tool supporting the design process. The tool directs the designer to specify all elements of the model in a consistent way. The specification is collected both by customized specification templates and by diagrams. The documentation and the diagram elements – both derived from the template information – are automatically generated. This prevents errors and provides specification consistency. Initial submission: 15 February 2002 / Revised submission: 20 September 2002 Published online: 2 December 2002 RID="*" ID="*"Supported by PROGRESS grant EES.5141 and ITEA DESS grant IT990211.     

An efficient distributed algorithm for constructing small dominating sets

The dominating set problem asks for a small subset D of nodes in a graph such that every node is either in D or adjacent to a node in D. This problem arises in a number of distributed network applications, where it is important to locate a small number of centers in the network such that every node is nearby at least one center. Finding a dominating set of minimum size is NP-complete, and the best known approximation is logarithmic in the maximum degree of the graph and is provided by the same simple greedy approach that gives the well-known logarithmic approximation result for the closely related set cover problem. We describe and analyze new randomized distributed algorithms for the dominating set problem that run in polylogarithmic time, independent of the diameter of the network, and that return a dominating set of size within a logarithmic factor from optimal, with high probability. In particular, our best algorithm runs in rounds with high probability, where n is the number of nodes, is one plus the maximum degree of any node, and each round involves a constant number of message exchanges among any two neighbors; the size of the dominating set obtained is within of the optimal in expectation and within of the optimal with high probability. We also describe generalizations to the weighted case and the case of multiple covering requirements. Received: January 2002 / Accepted: August 2002 RID="*" ID="*" Supported by NSF CAREER award NSF CCR-9983901 RID="*" ID="*" Supported by NSF CAREER award NSF CCR-9983901     

The meaning of multiplicity of n-ary associations in UML

The concept of multiplicity in UML derives from that of cardinality in entity-relationship modeling techniques. The UML documentation defines this concept but at the same time acknowledges some lack of obviousness in the specification of multiplicities for n-ary associations. This paper shows an ambiguity in the definition given by UML documentation and proposes a clarification to this definition, as well as the use of outer and inner multiplicities as a simple extension to the current notation to represent other multiplicity constraints, such as participation constraints, that are equally valuable in understanding n-ary associations. Initial submission: 16 January 2002 / Revised submission: 17 October 2002 Published online: 2 December 2002 RID="*" ID="*"A previous shorter version of this paper was presented under the title “Semantics of the Minimum Multiplicity in Ternary Associations in UML” at The 4th International Conference on the Unified Modeling Language-UML’2001, October 1–5 2001, Toronto, Ontario, Canada, Springer Verlag, LNCS 2185, pp. 329–341.     

Underflow revisited

Underflow is a floating-point phenomenon. Although the use of gradual underflow as defended in [2] and [3] is now widespread, most numerical analysts may not be aware of the fact that several implementations of the same principle are in existence, leading to different behavior of code on different platforms, mainly with respect to exception signaling. We intend to thoroughly discuss the slight differences among these implementations. Examples will be taken from current hardware and from our own multiprecision software class library. Throughout the discussion the focus is on the analysis of the phenomenon and not on any implementation issues. Many programmers are also unaware of the fact that the IEEE 754 and 854 standards do not guarantee that a program will deliver identical results on all conforming systems. Of all the differences that can occur cross-platform, the underflow exception is just one. Received: January 2002 / Accepted: June 2002 RID="*" ID="*"Research Director, FWO-Vlaanderen RID="**" ID="**"Supported by an NOI-grant from the Universiteit Antwerpen (UIA) RID="***" ID="***"Postdoctoral Fellow, FWO-Vlaanderen RID="****" ID="****"Research Fellow, IWT (Institute for Science and Technology)     

Relevance feedback in image retrieval: A comprehensive review

We analyze the nature of the relevance feedback problem in a continuous representation space in the context of content-based image retrieval. Emphasis is put on exploring the uniqueness of the problem and comparing the assumptions, implementations, and merits of various solutions in the literature. An attempt is made to compile a list of critical issues to consider when designing a relevance feedback algorithm. With a comprehensive review as the main portion, this paper also offers some novel solutions and perspectives throughout the discussion. RID="*" ID="*" Work was done while at the University of Illinois.     

Comments on deriving protocol specifications from service specifications written in LOTOS

Summary. An algorithm by Kant, Higashino and Bochmann for service-based protocol synthesis in the standard specification language LOTOS is discussed. It is demonstrated that the transformations for distributed implementation of synchronised parallel execution and of disabling are not correct in a general case. Received: January 1998 / Accepted: January 1999     

On the exponential representation problem

 The knowledge representation problem is understood as finding a reasonable joint distribution for a collection of marginal distributions. The problem is reformulated as a “moment problem”, and the solution is searched in the exponential form. Further, an equivalent parametrization is introduced with a parameter which can be easily identified even in higher dimensional cases. The problem of evaluating relevant model characteristics is discussed. RID="*" ID="*" Supported by grant GA ČR 102/99/1137.     

Constructing a video server with tertiary storage: Practice and experience

Handling a tertiary storage device, such as an optical disk library, in the framework of a disk-based stream service model, requires a sophisticated streaming model for the server, and it should consider the device-specific performance characteristics of tertiary storage. This paper discusses the design and implementation of a video server which uses tertiary storage as a source of media archiving. We have carefully designed the streaming mechanism for a server whose key functionalities include stream scheduling, disk caching and admission control. The stream scheduling model incorporates the tertiary media staging into a disk-based scheduling process, and also enhances the utilization of tertiary device bandwidth. The disk caching mechanism manages the limited capacity of the hard disk efficiently to guarantee the availability of media segments on the hard disk. The admission controller provides an adequate mechanism which decides upon the admission of a new request based on the current resource availability of the server. The proposed system has been implemented on a general-purpose operating system and it is fully operational. The design principles of the server are validated with real experiments, and the performance characteristics are analyzed. The results guide us on how servers with tertiary storage should be deployed effectively in a real environment. RID="*" ID="*" e-mail: hjcha@cs.yonsei.ac.kr     

Restoration by path concatenation: fast recovery of MPLS paths

A new general theory about restoration of network paths is first introduced. The theory pertains to restoration of shortest paths in a network following failure, e.g., we prove that a shortest path in a network after removing k edges is the concatenation of at most k+1 shortest paths in the original network. The theory is then combined with efficient path concatenation techniques in MPLS (multi-protocol label switching), to achieve powerful schemes for restoration in MPLS based networks. We thus transform MPLS into a flexible and robust method for forwarding packets in a network. Finally, the different schemes suggested are evaluated experimentally on three large networks (a large ISP, the AS graph of the Internet, and the full Internet topology). These experiments demonstrate that the restoration schemes perform well in actual topologies. Received: December 2001 / Accepted: July 2002 RID="*" ID="*" This research was supported by a grant from the Ministry of Science, Israel     

An improved lower bound for the time complexity of mutual exclusion

We establish a lower bound of remote memory references for N-process mutual exclusion algorithms based on reads, writes, or comparison primitives such as test-and-set and compare-and-swap. Our bound improves an earlier lower bound of established by Cypher. Our lower bound is of importance for two reasons. First, it almost matches the time complexity of the best known algorithms based on reads, writes, or comparison primitives. Second, our lower bound suggests that it is likely that, from an asymptotic standpoint, comparison primitives are no better than reads and writes when implementing local-spin mutual exclusion algorithms. Thus, comparison primitives may not be the best choice to provide in hardware if one is interested in scalable synchronization. Received: January 2002 / Accepted: September 2002 RID="*" ID="*" Work supported by NSF grants CCR 9732916, CCR 9972211, CCR 9988327, ITR 0082866, and CCR 0208289.     

A reconfigurable architecture for autonomous visual-navigation

Abstract. This paper describes the design of a reconfigurable architecture for implementing image processing algorithms. This architecture is a pipeline of small identical processing elements that contain a programmable logic device (FPGA) and double port memories. This processing system has been adapted to accelerate the computation of differential algorithms. The log-polar vision selectively reduces the amount of data to be processed and simplifies several vision algorithms, making possible their implementation using few hardware resources. The reconfigurable architecture design has been devoted to implementation, and has been employed in an autonomous platform, which has power consumption, size and weight restrictions. Two different vision algorithms have been implemented in the reconfigurable pipeline, for which some experimental results are shown. Received: 30 March 2001 / Accepted: 11 February 2002 RID="*" ID="*" This work has been supported by the Ministerio de Ciencia y Tecnología and FEDER under project TIC2001-3546 Correspondence to: J.A. Boluda     

Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN

The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited.     

Model-checking multi-threaded distributed Java programs

State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of synchronization, namely, the use of locks to protect shared data structures. This pattern of synchronization is particularly common in concurrent Java programs, because Java provides built-in locks. We describe the design of a new tool for state-less state-space exploration of Java programs that incorporates this reduction. We also describe an implementation of the reduction in Java PathFinder, a more traditional state-space exploration tool for Java programs. Published online: 2 October 2002 RID="*" ID="*"Present address: Computer Science Dept., SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA. The author gratefully acknowledges the support of ONR under Grants N00014-99-1-0358 and N00014-01-1-0109 and the support of NSF under Grant CCR-9876058.     

An Approach to Security Requirements Engineering for a High Assurance System*

Requirements specifications for high-assurance secure systems are rare in the open literature. This paper examines the development of a requirements document for a multilevel secure system that must meet stringent assurance and evaluation requirements. The system is designed to be secure, yet combines popular commercial components with specialised high-assurance ones. Functional and non-functional requirements pertinent to security are discussed. A multidimensional threat model is presented. The threat model accounts for the developmental and operational phases of system evolution and for each phase accounts for both physical and non-physical threats. We describe our team-based method for developing a requirements document and relate that process to techniques in requirements engineering. The system requirements document presented provides a calibration point for future security requirements engineering techniques intended to meet both functional and assurance goals. RID="*" ID="*"The views expressed in this paper are those of the authors and should not be construed to reflect those of their employers or the Department of Defense. This work was supported in part by the MSHN project of the DARPA/ITO Quorum programme and by the MYSEA project of the DARPA/ATO CHATS programme. Correspondence and offprint requests to: T. Levin, Department of Computer Science, Naval Postgraduate School, Monterey, CA 93943-5118, USA. Tel.: +1 831 656 2339; Fax: +1 831 656 2814; Email: levin@nps.navy.mil     

On constructing communication protocols from component-based service specifications

Constructing communication protocols from component service specifications, each of which specifies a subfunction of the target protocol, enables efficient development of a large and complex communication protocol. Concerning this construction, related techniques have been already proposed: integration of component protocol specifications into a single protocol specification and transformation of service specifications to protocol specifications. However, the integration needs special knowledge of communication protocols, and the transformation requires that a large and complex service specification should be developed as input to produce the target protocol. In order to cope with these problems, this paper proposes a new method which at first integrates component service specifications into a single service specification, and then transforms the service specification into the target protocol by a protocol synthesis technique. The most important point of view is that component integration is performed at the service specification level rather than the protocol specification level. Additionally, we define a class of ‘well-formed’ service specification which ensures correctness of the target protocol. As a result, the integration and transformation can be efficiently executed in small state space without special knowledge of communication protocols. Finally, we have shown the effectiveness of the proposed method by constructing a part of the real-life OSI protocol FTAM.     

Implementing the CORBA GIOP in a high-performance object request broker environment

The success of the Object Management Group's General Inter-ORB Protocol (GIOP) is leading to the desire to deploy GIOP in an ever-wider range of application areas, many of which are significantly more demanding than traditional areas in terms of performance. The well-known performance limitations of present day GIOP-based object request brokers (ORBs) are therefore increasingly being seen as a problem. To help address this problem, this paper discusses a GIOP implementation which has high performance and quality of service support as explicit goals. The implementation, which is embedded in a research ORB called Gopi, is modular and extensible in nature and includes novel optimization techniques which should be separately portable to other ORB environments. This paper focuses on the message protocol aspects of Gopi's GIOP implementation; higher layer issues such as marshalling and operation demultiplexing are not covered in detail. Figures are provided which position Gopi's GIOP performance against comparable ORBs. The paper also discusses some of the design decisions that have been made in the development of the GIOP protocol in the light of our implementation experience. Received: May 2000 / Accepted: December 2000     

Stochastic cooperative distributed grammar systems and random graphs

We introduce an alternative definition of random graphs as a language generated by a stochastic cooperating distributed grammar system. We show a relationship between our definition and four known definitions of random graphs, an example of using our model to prove graph-theoretic properties, and we define k-probabilistic model of random graphs as an extension. The first important acquisition of our definition is that only a small modification of a stochastic cooperating distributed grammar system may effect the substantial change of the generated random graph model. Other important result resides in the fact that our approach enables the use of a new proving technique in the random graph theory which is based on the generative paradigm inherent in the formal languages theory. Received: 14 May 2002 / 30 October 2002 RID="*" ID="*" Supported by the VEGA grant No. 1/7152/20.