waashk/acm huggingface dataset:
specification formalisms for component-based concurrent systems this project builds on my ongoing research into design formalisms for, and the automatic verification of, concurrent systems. the difficulties such systems pose for system engineers are well-known and result in large part from the the complexities of process interaction and the possibilities for nondeterminism. my work is motivated by a belief that mathematically rigorous specification and verification techniques will ultimately lead to better and easier-to-build concurrent systems.my specific research interests lie in the development of fully automatic analysis methods and process-algebraic design formalisms for modeling system behavior. i have worked on algorithms for checking properties of, and refinement relations between, system descriptions [ch93, cs93]; the implementation and release of a verification tool, the cwb- nc [cs96] (see http://www.cs.sunysb.edu/~rance to obtain the distribution); case studies [bcl99, ecb97]; and the formalization of system features, such as real time, probability, and priority, in process algebra [bcl99, cdsyar].the aims of this project include the development of expressive and usable formalisms for specifying and reasoning about properties of _open, component- based_ concurrent systems. more specifically, my colleagues and i have been investigating new approaches for describing component requirements and automated techniques for determining when finite-state components meet their requirements. the key topics under study include the following.**a temporal logic for open systems.** we are working on a notation for conveniently expressing properties constraining the behavior of open systems.**implicit specifications.** _implicit specifications_ use system _contexts,_ or "test harness," to define requirements for open systems. we are studying expressiveness issues and model-checking algorithms for such specifications.**automatic model-checker generation.** we have been developing a _model-checker generator_ that, given a temporal logic and "proof rules" for the logic, automatically produces an efficient model checker. rance cleaveland
on the vax/vms time-critical process scheduling  the vax/vms process schedule is briefly described. a simple priority-driven round-robin queuing model is then constructed to analyze the behavior of the time-critical processes of vax/vms under such a schedule.  mean and variance of the conditional response time of a process at a given priority are derived, conditioned on the amount of service time required by that process. numerical results are given with comparisons to the ordinary priority queuing systems.  y. t. wang
producing reusable object-oriented components: a domain-and-organization- specific perspective  developing reusable object-oriented software requires a designer to determine how to structure a software system so as to achieve the necessary functionality, while at the same time increasing the reuse potential of the software. we introduce a set of reusability metrics intended to be iteratively applied during the design and implementation parts of the software life-cycle to help guide the production and identification of reusable components. component identification centers on the application's domain, with reuse focusing specifically on an organization's future systems. our approach requires the developer to subjectively categorize classes, identify component boundaries, and specify where components are related. our metrics provide reuse valuations on the couplings between components. based upon the results of applying our metrics, we provide refactoring guidelines to increase the separation between components in a manner that improves component reusability. we include an application of our metrics to a commercial objec- oriented framework.  margaretha w. price donald m. needham steven a. demurjian
lustre: a declarative language for real-time programming  lustre is a synchronous data-flow language for programming systems which interact with their environments in real-time. after an informal presentation of the language, we describe its semantics by means of structural inference rules. moreover, we show how to use this semantics in order to generate efficient sequential code, namely, a finite state automaton which represents the control of the program. formal rules for program transformation are also presented.  p. caspi d. pilaud n. halbwachs j. a. plaice
on failure of the pruning technique in "error repair in shift-reduce parsers"  a previous article presented a technique to compute the least-cost error repair by incrementally generating configurations that result from inserting and deleting tokens a syntactically incorrect input. an additional mechanism to improve the run-time efficiency of this algorithm by pruning some of the configurations was discussed as well. in this communication we show that the pruning mechanism may lead to suboptimal repairs or may block all repairs. certain grammatical errors in a common construct of the java programming language also lead to the above kind of failure.  eberhard bertsch mark-jan nederhof
facade: a typed intermediate language dedicated to smart cards  the use of smart cards to run software modules on demand has become a major business concern for application issuers. such down-loadable executable content needs to be trusted by the card execution environment in order to ensure that an instruction on a memory area is compliant with the definition of the data stored in this area (i.e. its type). current solutions for smart cards rely on three techniques. for java card, either an off-card verifier- converter performs a static verification of type- safety, or a defensive virtual machine performs the verification at runtime. for other types of open smart cards, no type-checking is carried out and the trust is only based on the containment of applications. static verification is more efficient and flexible than dynamic techniques. nevertheless, as the java verifier cannot fit into a card, the trust is dependent on an external third- party. in this way, the card security has been partly turned to the outside. we propose and describe the facade language for which the type-safety verification can be performed statically on- card.  gilles grimaud jean-louis lanet jean-jacques vandewalle
info: interactive apl documentation a large body of apl code may be hard to understand and analyze, particularly if you are not its author. a code system that spans multiple workspaces (wss) compounds that problem._info_ is a multi- ws system written in apl+win that provides convenient interactive documentation of apl+win and apl+dos multi-ws systems. the user has a variety of displays that give insight into the system structures and relationships within single- or multi-ws systems. an administrator can easily set up and maintain the info static analysis data bases for any number of ws groups.this paper demonstrates info by showing how info documents itself. a distribution package contains the complete code and instructions for setting up this self- documentation. george mebus
describing distributed environments (abstract only)  the distributed execution analysis suite project (dea-suite) [1] is concerned with developing a set of integrated tools for studying the execution of programs in a distributed environment. dea-suite consists of an environment to: (1) allow the specification of a candidate distributed execution environment. (2) assign the distributable portions of a program to the sites of execution in the distributed execution environment. (3) schedule the distributable portions of a program as they become enabled, and finally (4) simulate the execution of the program on the candidate distributed execution environment. one aim is to provide an environments. the presentation's focus will be on the description of distributed environments within the dea-suite project.  paul a. ponville
software engineering tutorial  the field of software engineering has undergone some of the most profound changes in the last decade. in recent years, the national acm conferences have been giving increasing attention to software engineering---"structured program planning and design: standardization needs" (acm '79 - detroit) and " more on structured design" (acm '80 - nashville).  this session contains treatment of software engineering with emphasis on real applications. presented are state-of-the-art software techniques including the latest refinements in structured analysis and design and programming methodologies. several issues related to the portrayal of software design include architectural, structural, behavioral, and informational considerations. stressed are techniques for implementing reliable, maintainable software. also offered are software management approaches.  murray r. berkowitz gordon davis kenneth t. orr james a. senn darrell ward
new type signatures for legacy fortran subroutines we are currently developing a methodological framework for reverse engineering fortran77 programs used by electricite de france, in which the first step is the construction of an algebraic specification which faithfully represents the fortran code. to construct this specification, we must decide on a coherent set of "profiles" (type signatures) for the specifications of the fortran sub-programs. we propose an analysis of the dynamic aliases between formal and actual sub- program arguments in order to derive these profiles. in many examples of real fortran code this analysis does not give satisfactory results if arrays are treated as indivisible. instead, we must take into account which fragment of the array may really be accessed by the sub-program. we have therefore implemented our analysis as an extension of the _pips_ code parallelisation tool, which provides us with a precise analysis of inter- procedural array data-flow. nicky williams preston
orchestrating interactions among parallel computations  many parallel programs contain multiple sub-computations, each with distinct communication and load balancing requirements. the traditional approach to compiling such programs is to impose a processor synchronization barrier between sub- computations, optimizing each as a separate entity. this paper develops a methodology for managing the interactions among sub-computations, avoiding strict synchronization where concurrent or pipelined relationships are possible.  our approach to compiling parallel programs has two components: symbolic data access analysis and adaptive runtime support. we summarize the data access behavior of sub-computations (such as loop nests) and split them to expose concurrency and pipelining opportunities. the split transformation has been incorporated into an extended fortran compiler, which outputs a fortran 77 program augmented with calls to library routines written in c and a coarse- grained dataflow graph summarizing the exposed parallelism.  the compiler encodes symbolic information, including loop bounds and communication requirements, for an adaptive runtime system, which uses runtime information to improve the scheduling efficiency of irregular sub- computations. the runtime system incorporates algorithms that allocate processing resources to concurrently executing sub-computations and choose communication granularity. we have demonstrated that these dynamic techniques substantially improve performance on a range of production applications including climate modeling and x-ray tomography, expecially when large numbers of processors are available.  susan l. graham steven lucco oliver sharp
system development methodology using logos  the development of applications written in apl has traditionally both benefited by and suffered from the freedom offered by the environment. a consequence of this freedom is that few applications are designed from the perspectives of consistency, modularity, and structure. this paper describes how logos, a programming environment for apl, helps improve the development and maintenance of apl applications. through the use of basic support facilities and integrated tools, logos encourages a modular design within applications and a greater consistency among them. the support facilities provide such functionality as the paging of large applications, or the parallel testing of multiple versions of software, with minimal effort.  specific examples of system design and development are given in the paper. programming methodologies in widespread practice are examined, and their application to apl with logos is described. the use of logos in top-down design and in application prototyping is also discussed.  david b. allen mark r. dempsey leslie h. goldsmith
enumerated data types the origins of many language features are hard to pin down. not so with enumerated data types. these were invented by niklans wirth in the design of the pascal programming language [1]. they permit convenience and greater safety in performing tasks that had to handled by mapping concepts to a subrange of the integers in previous languages. the feature is useful enough and easy enough to define and implement that no really modem language is without some form of it.the feature is still missing from fortran. the proposed new standard for fortran adds a version of the feature to the language [2]. however, it is present as part of a c-interoperability mechanism only. unfortunately, it leaves out most of the aspects of the idea that make it useful to a programmer. and it is not even necessary for interoperation with c.this article describes the concept of enumerated data types and the properties the feature should include. it then describes the proposed version of the feature in fortran. some suggestions will be made about future directions. jim giles
software development process audits - a general procedure  to assist development organizations in improving software quality and productivity, the at&amp;t; bell laboratories quality assurance center created a design quality group to independently evaluate the software development processes and associated development products of our at&amp;t; projects. these software development process audits examine software engineering techniques and tools in practice, as they fit into the overall development environment. our strategy behind these audits is to assemble a team which, with the involvement of the developers and their managers, will: characterize the existing development process; identify project strengths and areas for improvements; and recommend possible improvements. this paper details the general approach behind this strategy.  stewart g. crawford m. hosein fallah
the design and implementation of tripwire: a file system integrity checker  at the heart of most computer systems is a file system. the file system contains user data, executable programs, configuration and authorization information, and (usually) the base executable version of the operating system itself. the ability to monitor file systems for unauthorized or unexpected changes gives system administrators valuable data for protecting and maintaining their systems. however, in environments of many networked heterogeneous platforms with different policies and software, the task of monitoring changes becomes quite daunting.  tripwire is tool that aids unix system administrators and users in monitoring a designated set of files and directories for any changes. used with system files on a regular (e.g., daily) basis, tripwire can notify system administrators of corrupted or altered files, so corrective actions may be taken in a timely manner. tripwire may also be used on user or group files or databases to signal changes.  this paper describes the design and implementation of the tripwire tool. it uses interchangeable "signature" (usually, message digest) routines to identify changes in files, and is highly configurable. tripwire is no-cost software, available on the internet, and is currently in use on thousands of machines around the world.  gene h. kim eugene h. spafford
error repair with validation in lr-based parsing when the compiler encounters an error symbol in an erroneous input, the local error-repair method repairs the input by either inserting a repair string before the error symbol or deleting the error symbol. although the extended fmq of fischer et al. and the method of mckenzie et al. report the improved quality of diagnostic messages, they suffer from redundant parse stack configurations.this article proposes an efficient lr error-recovery method, with validation-removing repairs that give the same validation result as a previously considered, lower-cost repair. moreover, its execution speed is proportional to the length of the stack configuration. the algorithm is implemented on a bison, gnu lalr(1), parser generating system. experimental results are presented. ik-soon kim kwang-moo choe
automatic determination of recommended test combinations for ada compilers  ada compilers are validated using the ada compiler validation capability (acvc) test suite, containing over 4000 individual test programs. each test program focuses, to the extent possible, on a single language feature. despite the advantages of this "atomic testing" methodology, it is often the unexpected interactions between language features that result in compilation problems. this research investigated techniques to automatically identify recommended combinations of ada languge features for compiler testing. a prototype program was developed to analyze the ada language grammar specification and generate a list of recommended combinations of features to be tested. the output from this program will be used within the ada features identification system (afis), a configuration management tool currently under development for the acvc test suite. the prototype uses an annotated ada language grammar to drive a test case generator. the generated combinations of ada features are analyzed to select the combinations to be tested. while the skill and intuition of the compiler tester are eseential to the annotation of the ada grammar, the prototype demonstrated that automated support tools can be used to identify recommended combinations for ada compiler testing.  james s. marr patricia k. lawlis
script: a communication abstraction mechanism  in this paper, we introduce a new abstraction mechanism, called a script, which hides the low-level details that implement patterns of communication. a script localizes the communication between a set of roles (formal processes), to which actual processes enroll in order to participate in the action of the script. the paper discusses the addition of scripts to the languages csp and ada, as well as to a shared-variable language with monitors.  nissim francez brent hailpern
improving the ratio of memory operations to floating-point operations in loops  over the past decade, microprocessor design strategies have focused on increasing the computational power on a single chip. because computations often require more data from cache per floating-point operation than a machine can deliver and because operations are pipelined, idle computational cycles are common when scientific applications are executed. to overcome these bottlenecks, programmers have learned to use a coding style that ensures a better balance between memory references and floating-point operations. in our view, this is a step in the wrong direction because it makes programs more machine-specific. a programmer should not be required to write a new program version for each new machine; instead, the task of specializing a program to a target machine should be left to the compiler.  but is our view practical? can a sophisticated optimizing compiler obviate the need for the myriad of programming tricks that have found their way into practice to improve the performance of the memory hierarchy? in this paper we attempt to answer that question. to do so, we develop and evaluate techniques that automatically restructure program loops to achieve high performance on specific target architectures. these methods attempt to balance computation and memory accesses and seek to eliminate or reduce pipeline interlock. to do this, they estimate statically the balance between memory operations and floating-point operations for each loop in a particular program and use these estimates to determine whether to apply various loop transformations.  experiments with our automatic techniques show that integer-factor speedups are possible on kernels. additionally, the estimate of the balance between memory operations and computation, and the application of the estimate are very accurate---experiments reveal little difference between the balance achieved by our automatic system that is made possible by hand optimization.  steve carr ken kennedy
practical applications of a syntax directed program manipulation environment  we present applications in various domains of a system built around a syntax directed editor: the mentor system.  the main characteristics of the system are the abstract representation of data, programmability of the command language, and language independance.  the applications presented belong to the area of program editing and manipulation, extensions of programming languages through the development of preprocessors, processing of multi-formalism documents and program portability.  v donzeau-gouge b. lang b. melese
using aspectc to improve the modularity of path-specific customization in operating system code layered architecture in operating system code is often compromised by execution path-specific customizations such as prefetching, page replacement and scheduling strategies. path-specific customizations are difficult to modularize in a layered architecture because they involve dynamic context passing and layer violations. effectively they are vertically integrated slices through the layers. an initial experiment using an aspect- oriented programming language to refactor prefetching in the freebsd operating system kernal shows significant benefits, including easy (un)pluggability of prefetching modes, independent development of prefetching modes, and overall improved comprehensibility. yvonne coady gregor kiczales mike feeley greg smolyn
microcomputer operating systems panel: unix  are multi-user microcomputer systems a good idea? they tend to be reinventions of the timesharing mainframe mistakes of the 60's and 70's. why not give each user a real micro? this argument leads one either to multiprocessor systems, or to networking.  but unix is an interesting system, since it's inherently multi-programmed, and because multi-programming if done correctly makes your system inherently multi-user. this is a case of the principle that if you make things general, you often get unexpected benefits.  unix also inherently facilitates sharing of files and other resources. other systems tend to make communal sharing difficult. unix evolved to serve a small community of cooperating users, hence a "supermicro" unix for a small department should work well (and does). unix has also, of course, been used in much larger (and less cooperative!) environments with considerable success (but not without some system maintenance).  ian f. darwin
spin \\- an extensible microkernel for application-specific operating system services application domains such as multimedia, databases, and parallel computing, require operating system services with high performance and high functionality. existing operating systems provide fixed interfaces and implementations to system services and resources. this makes them inappropriate for applications whose resource demands and usage patterns are poorly matched by the services provided. the _spin_ operating system enables system services to be defined in an application-specific fashion through an _extensible_ microkernel. it offers applications fine-grained control over a machine's logical and physical resources through run-time _adaptation_ of the system to application requirements. brian n. bershad craig chambers susan eggers chris maeda dylan mcnamee przemyslaw pardyak stefan savage emin gun sirer