bluuebunny/crossref_metadata_2025 huggingface dataset:
Alpha-structural recursion and induction
Authors: Pitts Andrew M.
Published: October 2006

The
nominal
approach to abstract syntax deals with the issues of bound names and α-equivalence by considering constructions and properties that are invariant with respect to permuting names. The use of permutations gives rise to an attractively simple formalization of common, but often technically incorrect uses of structural recursion and induction for abstract syntax modulo α-equivalence. At the heart of this approach is the notion of
finitely supported
mathematical objects. This article explains the idea in as concrete a way as possible and gives a new derivation within higher-order classical logic of principles of α-
structural
recursion and induction for α-equivalence classes from the ordinary versions of these principles for abstract syntax trees.
Logic program-based updates
Authors: Zhang Yan
Published: October 2006

In logic program-based updates, contradictory information elimination, conflict resolution, and syntactic representation are three major issues that interfere with each other and significantly influence the update result. We observe that existing approaches of logic program-based updates, in one way or another, are problematic to deal with these issues. In this article, we address all these problems in a systematic manner. Our approach to the logic program-based update has the following features: (1) a prioritized logic programming language is employed for providing a formal basis of formalizing logic program-based updates, so that information conflict and its related problems in updates can be handled properly; (2) our approach presents both semantic characterization and syntactic representation for the underlying update procedure, and hence is consistent with the nature of updates within the logic program extent-declarative semantics and syntactic sensitivity; and (3) our approach also provides nontrivial solutions to simplify various update evaluation procedures under certain conditions.
Fast verification of MLL proof nets via IMLL
Authors: Murawski Andrzej S. , Ong C.-H. Luke
Published: October 2006

We consider the following decision problems:ProofNet: Is a given multiplicative linear logic (MLL) proof structure a proof net?EssNet: Is a given essential net (of an intuitionistic MLL sequent) correct?In this article we show how to obtain linear-time algorithms for EssNet. As a corollary, by showing that ProofNet is linear-time reducible to EssNet (by the Trip Translation), we obtain a linear-time algorithm for ProofNet.We show further that it is possible to optimize the verification so that each node of the input structure is visited at most once. Finally, we present linear-time algorithms for
sequentializing
proof nets and essential nets, that is, for finding derivations of the underlying sequents.
Stanford WebBase components and applications
Authors: Cho Junghoo , Garcia-Molina Hector , Haveliwala Taher , Lam Wang , Paepcke Andreas , Raghavan Sriram , Wesley Gary
Published: October 2006

We describe the design and performance of WebBase, a tool for Web research. The system includes a highly customizable crawler, a repository for collected Web pages, an indexer for both text and link-related page features, and a high-speed content distribution facility. The distribution module enables researchers world-wide to retrieve pages from WebBase, and stream them across the Internet at high speed. The advantage for the researchers is that they need not all crawl the Web before beginning their research. WebBase has been used by scores of research and teaching organizations world-wide, mostly for investigations into Web topology and linguistic content analysis. After describing the system's architecture, we explain our engineering decisions for each of the WebBase components, and present respective performance measurements.
Models and solutions for radio irregularity in wireless sensor networks
Authors: Zhou Gang , He Tian , Krishnamurthy Sudha , Stankovic John A.
Published: October 2006

In this article, we investigate the impact of radio irregularity on wireless sensor networks. Radio irregularity is a common phenomenon that arises from multiple factors, such as variance in RF sending power and different path losses, depending on the direction of propagation. From our experiments, we discover that the variance in received signal strength is largely random; however, it exhibits a continuous change with incremental changes in direction. With empirical data obtained from the MICA2 and MICAZ platforms, we establish a radio model for simulation, called the Radio Irregularity Model (RIM). This model is the first to bridge the discrepancy between the spherical radio models used by simulators and the physical reality of radio signals. With this model, we investigate the impact of radio irregularity on several upper layer protocols, including MAC, routing, localization and topology control. Our results show that radio irregularity has a relatively larger impact on the routing layer than the MAC layer. It also shows that radio irregularity leads to larger localization errors and makes it harder to maintain communication connectivity in topology control. To deal with these issues, we present eight solutions to deal with radio irregularity. We evaluate three of them in detail. The results obtained from both the simulations and a running testbed demonstrate that our solutions greatly improve system performance in the presence of radio irregularity.
High-quality speech-to-speech translation for computer-aided language learning
Authors: Wang Chao , Seneff Stephanie
Published: October 2006

This article describes our research on spoken language translation aimed toward the application of computer aids for second language acquisition. The translation framework is incorporated into a multilingual dialogue system in which a student is able to engage in natural spoken interaction with the system in the foreign language, while speaking a query in their native tongue at any time to obtain a spoken translation for language assistance. Thus the quality of the translation must be extremely high, but the domain is restricted. Experiments were conducted in the weather information domain with the scenario of a native English speaker learning Mandarin Chinese. We were able to utilize a large corpus of English weather-domain queries to explore and compare a variety of translation strategies: formal, example-based, and statistical. Translation quality was manually evaluated on a test set of 695 spontaneous utterances. The best speech translation performance (89.9% correct, 6.1% incorrect, and 4.0% rejected), is achieved by a system which combines the formal and example-based methods, using parsability by a domain-specific Chinese grammar as a rejection criterion.
A monadic program slicer
Authors: Zhang Yingzhou , Gayo Jose Emilio Labra , del Río Agustín Cernuda
Published: October 2006

Program slicing is an important decomposition technique. It has been widely used in many software activities, such as software analyzing, understanding, debugging, testing, and maintenance. The current slicing methods and tools, however, are monolithic, and mainly based on program or system dependence graph. This paper presents a novel formal tool for program slicing. It abstracts the computation of program slicing as a language-independent slice monad transformer, which can be applied to the semantic descriptions of the program in a modular way, forming the corresponding slicing algorithms. Such algorithms allow program slices to be computed directly on abstract syntax, with no need to explicitly construct intermediate structures such as dependence graphs or to record an execution history. It has reusability and language-flexibility properties in comparison with the current program slicing methods/tools.
Minimizing mean flow time for UET tasks
Authors: Huo Yumei , Leung Joseph Y.-T.
Published: October 2006

We consider the problem of scheduling a set of
n
unit-execution-time (UET) tasks, with precedence constraints, on
m
≥ 1 parallel and identical processors so as to minimize the mean flow time. For two processors, the Coffman--Graham algorithm gives a schedule that simultaneously minimizes the mean flow time and the makespan. The problem becomes strongly NP-hard for an arbitrary number of processors, although the complexity is not known for each fixed
m
≥ 3. For arbitrary precedence constraints, we show that the Coffman--Graham algorithm gives a schedule with a worst-case bound no more than 2, and we give examples showing that the bound is tight. For intrees, the problem can be solved in polynomial time for each fixed
m
≥ 1, although the complexity is not known for an arbitrary number of processors. We show that Hu's algorithm (which is optimal for the makespan objective) yields a schedule with a worst-case bound no more than 1.5, and we give examples showing that the ratio can approach 1.308999.
An improved algorithm for CIOQ switches
Authors: Azar Yossi , Richter Yossi
Published: October 2006

The problem of maximizing the weighted throughput in various switching settings has been intensively studied recently through competitive analysis. To date, the most general model that has been investigated is the standard CIOQ (Combined Input and Output Queued) switch architecture with internal fabric speedup
S
≥ 1. CIOQ switches, that comprise the backbone of packet routing networks, are
N
×
N
switches controlled by a switching policy that incorporates two components: Admission control and scheduling. An admission control strategy is essential to determine the packets stored in the FIFO queues in input and output ports, while the scheduling policy conducts the transfer of packets through the internal fabric, from input ports to output ports. The online problem of maximizing the total weighted throughput of CIOQ switches was recently investigated by Kesselman and Rosén [2003]. They presented two different online algorithms for the general problem that achieve non-constant competitive ratios (linear in either the speedup or the number of distinct values, or logarithmic in the value range). We introduce the first constant-competitive algorithm for the general case of the problem, with arbitrary speedup and packet values. Specifically, our algorithm is 8-competitive, and is also simple and easy to implement.
Home turf
Authors: Shannon Meg McGinity
Published: October 2006

Service providers are building their networks right to your door---that is, your den, your bedroom, and your kitchen.
VAMNET
Authors: Bosse Stefan
Published: October 2006

This article gives a design overview of a new reliable distributed operating system environment, combining the world of functional and distributed programming using a virtual machine approach for hiding system dependencies, offering rapid prototyping facilities. The basic operating system concepts used are derived from the Amoeba operating system by Andrew Tanenbaum and his work group, developed 20 years ago. VAMNET is not only a native operating system. It is a hybrid solution for expanding widely used operating systems like UNIX with a distributed execution environment.
Towards automatic social bootstrapping of peer-to-peer protocols
Authors: Hales David , Babaoglu Ozalp
Published: October 2006

Current peer-to-peer systems rely on user intervention to install and update the software (protocols) that run on each node. We propose another direction where protocols are dynamically and automatically rolled-out over peers, with the peers themselves selecting those that are beneficial and rejecting those which are not. To achieve this, we argue that, new protocols should be "injected" live into a running P2P system, with peers themselves replicating them. This requires that peers select "socially beneficial" protocols even though they need to base this on their own individual performance evaluations. What we are proposing can be seen as a meta-protocol, which we call
Automatic Social Bootstrapping
, that intelligently selects and replicates those protocols that are for the social good --- that is, maximize the average utility of the entire population. We sketch an outline of the protocol and present some initial high-level simulation results. Finally we identify several open issues that need to be addressed in order to further develop the approach.
Accountability protocols
Authors: Bella Giampaolo , Paulson Lawrence C.
Published: October 2006

Classical security protocols aim to achieve authentication and confidentiality under the assumption that the peers behave honestly. Some recent protocols are required to achieve their goals even if the peer misbehaves.
Accountability
is a protocol design strategy that may help. It delivers to peers sufficient evidence of each other's participation in the protocol. Accountability underlies the nonrepudiation protocol of Zhou and Gollmann and the certified email protocol of Abadi et al. This paper provides a comparative, formal analysis of the two protocols, and confirms that they reach their goals under realistic conditions. The treatment, which is conducted with mechanized support from the proof assistant Isabelle, requires various extensions to the existing analysis method. A byproduct is an account of the concept of
higher-level protocol
.
Designing DCCP
Authors: Kohler Eddie , Handley Mark , Floyd Sally
Published: October 2006

Fast-growing Internet applications like streaming media and telephony prefer timeliness to reliability, making TCP a poor fit. Unfortunately, UDP, the natural alternative, lacks congestion control. High-bandwidth UDP applications must implement congestion control themselves-a difficult task-or risk rendering congested networks unusable. We set out to ease the safe deployment of these applications by designing a
congestion-controlled unreliable transport protocol
. The outcome, the Datagram Congestion Control Protocol or DCCP, adds to a UDP-like foundation the minimum mechanisms necessary to support congestion control. We thought those mechanisms would resemble TCP's, but without reliability and, especially, cumulative acknowledgements, we had to reconsider almost every aspect of TCP's design. The resulting protocol sheds light on how congestion control interacts with unreliable transport, how modern network constraints impact protocol design, and how TCP's reliable bytestream semantics intertwine with its other mechanisms, including congestion control.
Enabling contribution awareness in an overlay broadcasting system
Authors: Sung Yu-Wei , Bishop Michael , Rao Sanjay
Published: October 2006

We consider the design of bandwidth-demanding broadcasting applications using overlays in environments characterized by hosts with limited and asymmetric bandwidth, and significant heterogeneity in outgoing bandwidth. Such environments are critical to consider to extend the applicability of overlay multicast to mainstream Internet environments where insufficient bandwidth exists to support all hosts, but have not received adequate attention from the research community. We leverage the multi-tree framework and design heuristics to enable it to consider host contribution and operate in bandwidth-scarce environments. Our extensions seek to simultaneously achieve good utilization of system resources, performance to hosts commensurate to their contributions, and consistent performance. We have implemented the system and conducted an Internet evaluation on Planet-Lab using real traces from previous operational deployments of an overlay broadcasting system. Our results indicate for these traces, our heuristics can improve the performance of high contributors by 10-240% and facilitate equitable bandwidth distribution among hosts with similar contributions.
The Liberty Simulation Environment
Authors: Vachharajani Manish , Vachharajani Neil , Penry David A. , Blome Jason A. , Malik Sharad , August David I.
Published: October 2006

In digital hardware system design, the quality of the product is directly related to the number of meaningful design alternatives properly considered. Unfortunately, existing modeling methodologies and tools have properties which make them less than ideal for rapid and accurate design-space exploration. This article identifies and evaluates the shortcomings of existing methods to motivate the Liberty Simulation Environment (LSE). LSE is a high-level modeling tool engineered to address these limitations, allowing for the rapid construction of accurate high-level simulation models. LSE simplifies model specification with low-overhead component-based reuse techniques and an abstraction for timing control. As part of a detailed description of LSE, this article presents these features, their impact on model specification effort, their implementation, and optimizations created to mitigate their otherwise deleterious impact on simulator execution performance.
A pragmatic HCI approach
Authors: Cox David
Published: October 2006

In order to provide effective human interaction with a computer interface, the design process must consider human cognitive factors. From an educational perspective, this area encompasses a range of issues which, because of academic time constraints, might be difficult to focus on, particularly if practical design and implementation are part of the syllabus. The paper describes how focusing on one area of perception with unusual and challenging perceptual images promoted quick interface design, provided stimulation for programming a working interface and highlighted the value of factors such as perception and affordance in the design of screen objects. A later formal series of questions revealed that learners saw the importance of human factors and the relevance of such issues in the design process as well as providing an incentive for programming a working model.
Teaching ethics in a virtual classroom
Authors: Goold Annegret , Coldwell Jo
Published: October 2006

This paper describes an ethics course that is a capstone course in the undergraduate computing degree at Deakin University. What distinguishes this course from others is that it has a fairly large enrolment of students and it is delivered completely online. The students enrolled in the course come from a variety of backgrounds and many are international students for whom English is not their first language. The paper describes the course, how it has evolved over a five-year period and discusses the rationale and particulars of course content and implementation in the 'virtual classroom'. Some of the challenges and issues for teaching a course of this type are discussed. Suggestions are offered for faculty who are considering the implementation of a similar course online.
You can lead a horse to water
Authors: Stern Linda , Markham Selby , Hanewald Ria
Published: October 2006

A great deal of effort is expended creating multimedia systems to help students learn. Some amount of effort is spent evaluating learning outcomes for students who have used these systems. Yet very little effort is spent examining how students actually use the software or how learning outcomes are related to system design. In a study involving direct observation of university students as they used pedagogical software, it was found that students develop their own strategies for learning with software and that these strategies are not necessarily those predicted by software designers and educators. Systematic field observation led to a more comprehensive view of how students were interacting with the software.
Principles of curriculum design and revision
Authors: Krishna Rao M. R. K. , Junaidu S. , Maghrabi T. , Shafique M. , Ahmed M. , Faisal K.
Published: October 2006

Our department has recently revisited its computer science program in the light of IEEE/ACM Computing Curricula 2001 (CC2001) recommendations, taking into consideration the ABET's Criteria for Accrediting Computing programs (CAC 04-05). The effort resulted in a revised curriculum. This paper presents the different decisions we made with regard to the curriculum orientation, knowledge units coverage, transition management, and monitoring and assessment. The paper also sheds some light on challenges faced. Tables provided in the paper show that the curriculum successfully implements CC2001 recommendations while satisfying the CAC 04-05.
When do group projects widen the student experience gap?
Authors: Barker Lecia J.
Published: October 2006

This paper presents a case study as a "cautionary tale" to faculty, demonstrating how students and instructors often perceive pressure to finish projects for clients. As a result of this pressure, and because students generally lacked any understanding of how to work well in groups, students selected their roles based on expediency or familiarity. This worked against the benefits of collaborative learning and learning new skills or concepts, widening the experience gap between males and females and across disciplines. Faculty should carefully consider the learning outcomes expected for students and find ways of ensuring they are achieved.
Student communication challenges in distributed software engineering environments
Authors: Woit D. , Bell K.
Published: October 2006

We investigate Non-Face-to-Face (NFtF) distributed collaboration in a population for which technology poses no barrier-students involved in distributed software engineering via Distance Learning. Our study finds students believe themselves significantly less effective in this environment because of lack of traditional non-verbal cues, in partial agreement with previous work. Based on our results, we identify potential problems and present activities to mitigate these so that NFtF oriented interactions may be made more effective for this group.
Teaching programming collaboratively
Authors: Flood Raymond , Lockhart Bob
Published: October 2006

We describe a collaborative approach to teaching core programming concepts based on student debate and involving the Phoenix meta-language generator.
Teaching polymorphism early
Authors: Bergin Joseph , Wallingford Eugene , Caspersen Michael , Goldweber Michael , Kolling Michael
Published: October 2006

Is it possible to teach dynamic polymorphism early? What techniques could facilitate teaching it in Java. This panel will bring together people who have considered this question and attempted to implement it in various ways, some more completely than others. It will also give participants an opportunity to explore the topic and to share their own ideas.
Students evaluating faculty
Authors: Carrasquel Jacobo
Published: October 2006

A common practice in colleges and universities across the US is to have students evaluate their faculty members. These evaluations, in most cases, are used for reappointments, promotions, and salary rises. For a longtime, I have believed that this system is subjective to many factors that have nothing to do with the quality and effectiveness of the faculty member. Other research has demonstrated that these evaluations depend of gender, course difficulty, grade expectancy, and other well know factors. This paper is the result of conducting student evaluations every 3 weeks during my last semester of teaching. The data will show that my evaluations fluctuate depending of many factors like weather, difficulty of assignments, mid-semester break, and students' mood.
Computing history
Authors: Hemmendinger David
Published: October 2006

This poster describes a course on the history of computing, designed for both a computer science program and for general undergraduate education.
Introducing recursion by using multimedia
Authors: Rosenthal Tammy
Published: October 2006

This poster presents our experience in introducing recursion by using multimedia.
Toward integrating computing concepts into the K-12 curriculum
Authors: Hood Cynthia S. , Hood Dennis J.
Published: October 2006

A key to achieving widespread IT fluency is to make it part of the K-12 curriculum. Along these lines, there have been significant, ongoing efforts to motivate and establish standards for both students and teachers. This paper describes our experiences teaching K-12 teachers technology concepts.
Use of flash movies for teaching GUI programming
Authors: Pais Rui , Barros João Paulo
Published: October 2006

This paper proposes the use of Flash movies when introducing students to the use of a complex Integrated Development Environment in the context of a GUI programming course.
TS-05
Authors: Christensen Henrik Bærbak
Published: October 2006

In the short time span available in a software architecture course, it is difficult to find a software system that is both interesting from an architectural perspective and so small that it does not overwhelm the students.We present TS-05 which is a bare 150 line Java "toy-system" that never-the-less exhibits architectural complexity and challenges that emphasize the usefulness of architectural concepts, primarily
views
,
quality attributes
and
connectors
.
Hacking as a form of "self-improvement"
Authors: Clark Eric
Published: October 2006

When does hacking one's own property pose an ethical problem?
MindMapX
Authors: Davis Leon
Published: October 2006

Mind Mapping is a diagramming technique that allows its users to effectively capture, learn, manipulate and develop information. It has the potential to radically enhance an individual's capacity to learn, in both a single user and group environment and has been proven to do so in a wide variety of fields. MindMapX is a multi user Mind Mapping application that is being developed with the express intention of unlocking Mind Mapping's potential.
SoundSpaces
Authors: Gomes Raquel , Seabra Ricardo , Ventura João , Guedes Nuno
Published: October 2006

The SoundSpaces project in general serves as a framework to develop highly interactive and non-deterministic multimedia applications without the need to have programming or technical skills.
Integrating views on ethical behavior for computer professionals in an interdisciplinary environment
Authors: Walls David C.
Published: October 2006

This poster explores the connections among the ideas presented in several well-known papers and shows that, taken together, they provide a justification and guideline for the creation of a new standard of practice for those involved in the production of complex systems.
A Semantic Web ontology for context-based classification and retrieval of music resources
Authors: Ferrara Alfio , Ludovico Luca A. , Montanelli Stefano , Castano Silvana , Haus Goffredo
Published: October 2006

In this article, we describe the MX-Onto ontology for providing a Semantic Web compatible representation of music resources based on their context. The context representation is realized by means of an OWL ontology that describes music information and that defines rules and classes for a flexible genre classification. By flexible classification we mean that the proposed approach enables capturing the subjective interpretation of music genres by defining multiple membership relations between a music resource and the corresponding music genres, thus supporting context-based and proximity-based search of music resources.
Handling multiple points of view in a multimedia data warehouse
Authors: Arigon Anne-Muriel , Tchounikine Anne , Miquel Maryvonne
Published: October 2006

Data warehouses are dedicated to collecting heterogeneous and distributed data in order to perform decision analysis. Based on multidimensional model, OLAP commercial environments such as they are currently designed in traditional applications are used to provide means for the analysis of facts that are depicted by numeric data (e.g., sales depicted by amount or quantity sold). However, in numerous fields, like in medical or bioinformatics, multimedia data are used as valuable information in the decisional process. One of the problems when integrating multimedia data as facts in a multidimensional model is to deal with dimensions built on descriptors that can be obtained by various computation modes on raw multimedia data. Taking into account these computation modes makes possible the characterization of the data by various points of view depending on the user's profile, his best-practices, his level of expertise, and so on. We propose a new multidimensional model that integrates functional dimension versions allowing the descriptors of the multidimensional data to be computed by different functions. With this approach, the user is able to obtain and choose multiple points of view on the data he analyses. This model is used to develop an OLAP application for navigation into a hypercube integrating various functional dimension versions for the calculus of descriptors in a medical use case.
Oracles for bounded-length shortest paths in planar graphs
Authors: Kowalik Lukasz , Kurowski Maciej
Published: October 2006

We present a new approach for answering short path queries in planar graphs. For any fixed constant
k
and a given unweighted planar graph
G
= (
V
,
E
), one can build in O(|V|) time a data structure, which allows to check in O(1) time whether two given vertices are at distance at most
k
in
G
and if so a shortest path between them is returned. Graph
G
can be undirected as well as directed.Our data structure works in fully dynamic environment. It can be updated in O(1) time after removing an edge or a vertex while updating after an edge insertion takes polylogarithmic amortized time. Besides deleting elements one can also disable ones for some time. It is motivated by a practical situation where nodes or links of a network may be temporarily out of service.Our results can be easily generalized to other wide classes of graphs---for instance we can take any minor-closed family of graphs.
Secure multiparty computation of approximations
Authors: Feigenbaum Joan , Ishai Yuval , Malkin Tal , Nissim Kobbi , Strauss Martin J. , Wright Rebecca N.
Published: October 2006

Approximation algorithms can sometimes provide efficient solutions when no efficient exact computation is known. In particular, approximations are often useful in a distributed setting where the inputs are held by different parties and may be extremely large. Furthermore, for some applications, the parties want to compute a function of their inputs securely without revealing more information than necessary. In this work, we study the question of simultaneously addressing the above efficiency and security concerns via what we call
secure approximations.
We start by extending standard definitions of secure (exact) computation to the setting of secure approximations. Our definitions guarantee that no additional information is revealed by the approximation beyond what follows from the output of the function being approximated. We then study the complexity of specific secure approximation problems. In particular, we obtain a sublinear-communication protocol for securely approximating the Hamming distance and a polynomial-time protocol for securely approximating the permanent and related #P-hard problems.
Faster WCET flow analysis by program slicing
Authors: Sandberg Christer , Ermedahl Andreas , Gustafsson Jan , Lisper Björn
Published: October 2006

Static Worst-Case Execution Time (WCET) analysis is a technique to derive upper bounds for the execution times of programs. Such bounds are crucial when designing and verifying real-time systems. WCET analysis needs a program flow analysis to derive constraints on the possible execution paths of the analysed program, like iteration bounds for loops and dependences between conditionals.Current WCET analysis tools typically obtain flow information through manual annotations. Better support for automatic flow analysis would eliminate much of the need for this laborious work. However, to automatically derive high-quality flow information is hard, and solution techniques with large time and space complexity are often required.In this paper we describe how to use program slicing to reduce the computational need of flow analysis methods. The slicing identifes statements and variables which are guaranteed not to influence the program flow. When these are removed, the calculation time of our different flow analyses decreases, in some cases considerably.We also show how program slicing can be used to identify the input variables and globals that control the outcome of a particular loop or conditional. This should be valuable aid when performing WCET analysis and systematic testing of large and complex real-time programs.
Efficient code generation from SHIM models
Authors: Edwards Stephen A. , Tardieu Olivier
Published: October 2006

Programming concurrent systems is substantially more difficult than programming sequential systems, yet most embedded systems need concurrency. We believe this should be addressed through higher-level models of concurrency that eliminate many of the usual challenges, such as nondeterminism arising from races.The
shim
model of computation provides deterministic concurrency, and there already exist ways of implementing it in hardware and software. In this work, we describe how to produce more efficient C code from
shim
systems.We propose two techniques: a largely mechanical one that produces tail-recursive code for simulating concurrency, and a more clever one that statically analyzes the communication pattern of multiple processes to produce code with far less overhead. Experimentally, we find our tail-recursive technique produces code that runs roughly twice as fast as a baseline; our statically-scheduled code can run up to twelve times faster.
Generating optimized code from SCR specifications
Authors: Rothamel Tom , Liu Yanhong A. , Heitmeyer Constance L. , Leonard Elizabeth I.
Published: October 2006

A promising trend in software development is the increasing adoption of model-driven design. In this approach, a developer first constructs an abstract model of the required program behavior in a language, such as Statecharts or Stateflow, and then uses a code generator to automatically transform the model into an executable program. This approach has many advantages---typically, a model is not only more concise than code and hence more understandable, it is also more amenable to mechanized analysis. Moreover, automatic generation of code from a model usually produces code with fewer errors than hand-crafted code.One serious problem, however, is that a code generator may produce inefficient code. To address this problem, this paper describes a method for generating efficient code from SCR (Software Cost Reduction) specifications. While the SCR tabular notation and tools have been used successfully to specify, simulate, and verify numerous embedded systems, until now SCR has lacked an automated method for generating optimized code. This paper describes an efficient method for automatic code generation from SCR specifications, together with an implementation and an experimental evaluation. The method first synthesizes an execution-flow graph from the specification, then applies three optimizations to the graph, namely, input slicing, simplification, and output slicing, and then automatically generates code from the optimized graph. Experiments on seven benchmarks demonstrate that the method produces significant performance improvements in code generated from large specifications. Moreover, code generation is relatively fast, and the code produced is relatively compact.
Static typing for a faulty lambda calculus
Authors: Walker David , Mackey Lester , Ligatti Jay , Reis George A. , August David I.
Published: October 2006

A
transient hardware fault
occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such transient faults will cause any significant damage may seem remote, over the last several years transient faults have caused costly failures in high-end machines at America Online, eBay, and the Los Alamos Neutron Science Center, among others [6, 44, 15]. Because susceptibility to transient faults is proportional to the size and density of transistors, the problem of transient faults will become increasingly important in the coming decades.This paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines λzap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, λzap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally [10, 20, 30, 31, 32, 33, 41].To ensure that programs maintain the proper invariants and use λzap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that λzap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into λzap.
Transactional events
Authors: Donnelly Kevin , Fluet Matthew
Published: October 2006

Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events, which combines first-class synchronous messagepassing events with all-or-nothing transactions. This combination enables simple solutions to interesting problems in concurrent programming. For example, guarded synchronous receive can be implemented as an abstract transactional event, whereas in other languages it requires a non-abstract, non-modular protocol. Likewise, three-way rendezvous can also be implemented as an abstract transactional event, which is impossible using first-class events alone. Both solutions are easy to code and easy to reason about.The expressive power of transactional events arises from a sequencing combinator whose semantics enforces an all-or-nothing transactional property - either both of the constituent events synchronize in sequence or neither of them synchronizes. This sequencing combinator, along with a non-deterministic choice combinator, gives transactional events the compositional structure of a monad-with-plus. We provide a formal semantics for and a preliminary implementation of transactional events.
Modular development of certified program verifiers with a proof assistant
Authors: Chlipala Adam
Published: October 2006

I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. I take advantage of Coq's support for programming with dependent types and modules in the structure of my development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it's possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.
A pattern for almost compositional functions
Authors: Bringert Björn , Ranta Aarne
Published: October 2006

This paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here "almost compositional" means that for a number of the constructors in the type(s), the result of the function depends only on the constructor and the results of calling the function on the constructor's arguments. The pattern consists of a generic part constructed once for each data type or family of data types, and a task-specific part. The generic part contains the code for the predictable compositional cases, leaving the interesting work to the task-specific part. Examples of the pattern implemented in dependent type theory with inductive families, in Haskell with generalized algebraic data types and rank-2 polymorphism, and in Java using a variant of the Visitor design pattern are given. The relationship to the "Scrap Your Boilerplate" approach to generic programming, and to general tree types in dependent type theory are also investigated.
Algebraic fusion of functions with an accumulating parameter and its improvement
Authors: Katsumata Shin-ya , Nishimura Susumu
Published: October 2006

We present a unifying solution to the problem of fusion of functions, where both the producer function and the consumer function have one accumulating parameter. The key idea in this development is to formulate the producer function as a function which computes over a monoid of
data contexts
. Upon this formulation, we develop a fusion method called
algebraic fusion
based on the elementary theory of universal algebra and monoids. The producer function is fused with a monoid homomorphism that is derived from the definition of the consumer function, and is turned into a higher-order function f that computes over the monoid of endofunctions.We then introduce a general concept called
improvement
, in order to reduce the cost of computing over the monoid of endofunctions (i. e., function closures). An improvement of the function f via a monoid homomorphism
h
is a function
g
that satisfies
f =h
ºg. This provides a principled way of finding a first-order function representing a solution to the fusion problem. It also presents a clean and unifying account for varying fusion methods that have been proposed so far. Furthermore, we show that our method extends to support partial and infinite data structures, by means of an appropriate monoid structure.
Extensible programming with first-class cases
Authors: Blume Matthias , Acar Umut A. , Chae Wonseok
Published: October 2006

We present language mechanisms for polymorphic, extensible records and their exact dual, polymorphic sums with extensible first-class cases. These features make it possible to easily extend existing code with new cases. In fact, such extensions do not require any changes to code that adheres to a particular programming style. Using that style, individual extensions can be written independently and later be composed to form larger components. These language mechanisms provide a solution to the expression problem.We study the proposed mechanisms in the context of an implicitly typed, purely functional language PolyR. We give a type system for the language and provide rules for a 2-phase transformation: first into an explicitly typed λ-calculus with record polymorphism, and finally to efficient index-passing code. The first phase eliminates sums and cases by taking advantage of the duality with records.We implement a version of
PolyR
extended with imperative features and pattern matching - we call this language
MLPolyR
. Programs in
MLPolyR
require no type annotations - the implementation employs a reconstruction algorithm to infer all types. The compiler generates machine code (currently for PowerPC) and optimizes the representation of sums by eliminating closures generated by the dual construction.
Compliance Deconstructed
Authors: Cannon J. C. , Byers Marilee
Published: October 2006

The topic of compliance becomes increasingly complex each year. Dozens of regulatory requirements can affect a company’s business processes. Moreover, these requirements are often vague and confusing. When those in charge of compliance are asked if their business processes are in compliance, it is understandably difficult for them to respond succinctly and with confidence. This article looks at how companies can deconstruct compliance, dealing with it in a systematic fashion and applying technology to automate compliance-related business processes. It also looks specifically at how Microsoft approaches compliance to SOX.
Review of "Refactoring Databases: Evolutionary Database Design by Scott Ambler and Pramodkumar Sadalage," Addison-Wesley Professional, 2006, $49.99, ISBN: 0321293533.
Authors: Jovanovic Vladan
Published: October 2006

Review of "Refactoring Databases: Evolutionary Database Design by Scott Ambler and Pramodkumar Sadalage," Addison-Wesley Professional, 2006, $49.99, ISBN: 0321293533.
Seeking Compliance Nirvana
Authors: Nolann Greg A.
Published: October 2006

Compliance. The mere mention of it brings to mind a harrowing list of questions and concerns. For example, who is complying and with what? With so many standards, laws, angles, intersections, overlaps, and consequences, who ultimately gets to determine if you are compliant or not? How do you determine what is in scope and what is not? And why do you instantly think of an audit when you hear the word compliance? To see the tangled hairball that is compliance, just take a look at my company. It is on the hook for SOX, as we are a publicly traded company; for a number of banks for the PCI DSS, also known as Visa CISP; for HIPAA; for CA 1786; and for the European Union, its member countries, Japan, Korea, and a handful of other countries’ privacy and data security laws.
Information systems research with an attitude
Authors: Glassberg Bonnie C. , Grover Varun , Teng James T. C.
Published: October 2006

Attitudes have been uniquely defined by each discipline that uses them and information systems (IS) research is no exception. While traditional IS research looks at attitudes toward a behavior, consumer research pursues attitudes towards objects. This study applies concepts from marketing to formalize and operationalize Attitude consistent with the marketing perspective as involvement, including both cognitive and emotional evaluations. This broader, consumer-oriented conceptualization is empirically validated within a well established nomological network of technology acceptance constructs. Our study offers researchers a new rationale for the inclusion of an attitude measure in IS Research.
A case for a complexity-effective, width-partitioned microarchitecture
Authors: Rochecouste Olivier , Pokam Gilles , Seznec André
Published: October 2006

The analysis of program executions reveals that most integer and multimedia applications make heavy use of narrow-width operations, i.e., instructions exclusively using narrow-width operands and producing a narrow-width result. Moreover, this usage is relatively well distributed over the application. We observed this program property on the MediaBench and SPEC2000 benchmarks with about 40% of the instructions being narrow-width operations. Current superscalar processors use 64-bit datapaths to execute all the instructions of the applications. In this paper, we suggest the use of a width-partitioned microarchitecture (WPM) to master the hardware complexity of a superscalar processor. For a four-way issue machine, we split the processor in two two-way clusters: the main cluster executing 64-bit operations, load/store, and complex operations and a narrow cluster executing the 16-bit operations. We resort to partitioning to decouple the treatment of the narrow-width operations from that of the other program instructions. This provides the benefit of greatly simplifying the design of the critical processor components in each cluster (e.g., the register file and the bypass network). The dynamic interleaving of the two instruction types allows maintaining the workload balanced among clusters. WPM also helps to reduce the complexity of the interconnection fabric and of the issue logic. In fact, since the 16-bit cluster can only communicate narrow-width data, the datapath-width of the interconnect fabric can be significantly reduced, yielding a corresponding saving of the interconnect power and area. We explore different possible configurations of WPM, discussing the various implementation tradeoffs. We also examine a speculative steering heuristic to distribute the narrow-width operations among clusters. A detailed analysis of the complexity factors shows using WPM instead of a classical 64-bit two-cluster microarchitecture can save power and silicon area with a minimal impact on the overall performance.