Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 30 of 39

Full-Text Articles in Computer Engineering

Towards Overhead-Free Interface Theory For Compositional Hierarchical Real-Time Systems, Jin Hyun Kim, Kygong Hoon Kim, Arvind Easwaran, Insup Lee May 2018

Towards Overhead-Free Interface Theory For Compositional Hierarchical Real-Time Systems, Jin Hyun Kim, Kygong Hoon Kim, Arvind Easwaran, Insup Lee

Technical Reports (CIS)

Much recent research has been conducted on compositional real-time scheduling framework as the framework becomes a useful fundamental theory for real-time OS-Hypervisor. Much recent research has been conducted on compositional real-time scheduling as the framework becomes a useful fundamental theory for real-time OS-Hypervisor. However, compositional frameworks suffer from abstraction overheads in composing components. In this paper, we classify the composition overheads into i) supply abstraction overhead associated with the supply from a resource provider, and ii) demand abstraction overhead associated with the component workload. Then, we provide sufficient conditions for each abstraction overhead to be eliminated. In addition, this paper ...


Automated Bug Removal For Software-Defined Networks, Yang Wu, Andreas Haeberlen, Wenchao Zhou, Boon T. Loo, Ang Chen Jul 2017

Automated Bug Removal For Software-Defined Networks, Yang Wu, Andreas Haeberlen, Wenchao Zhou, Boon T. Loo, Ang Chen

Technical Reports (CIS)

When debugging an SDN application, diagnosing the problem is merely the first step: the operator must still find a fix that solves the problem, without causing new problems elsewhere. However, most existing debuggers focus exclusively on diagnosis and offer the network operator little or no help with finding an effective fix. Finding a suitable fix is difficult because the number of candidates can be enormous. In this paper, we propose a step towards automated repair for SDN applications. Our approach consists of two elements. The first is a data structure that we call meta provenance, which can be used to ...


Dstress: Efficient Differentially Private Computations On Distributed Data, Antonis Papadimitriou, Andreas Haeberlen, Arjun Narayan Jun 2017

Dstress: Efficient Differentially Private Computations On Distributed Data, Antonis Papadimitriou, Andreas Haeberlen, Arjun Narayan

Technical Reports (CIS)

In this paper, we present DStress, a system that can efficiently perform computations on graphs that contain confidential data. DStress assumes that the graph is physically distributed across many participants, and that each participant only knows a small subgraph; it protects privacy by enforcing tight, provable limits on how much each participant can learn about the rest of the graph. We also study one concrete instance of this problem: measuring systemic risk in financial networks. Systemic risk is the likelihood of cascading bankruptcies – as, e.g., during the financial crisis of 2008 – and it can be quantified based on the ...


Big Data Analytics Over Encrypted Datasets With Seabed, Antonis Papadimitriou, Ranjita Bhagwan, Nishanth Chandran, Ramachandran Ramjee, Andreas Haberlen, Harmeet Singh, Abhishek Modi, Saikrishna Badrinarayanan Oct 2016

Big Data Analytics Over Encrypted Datasets With Seabed, Antonis Papadimitriou, Ranjita Bhagwan, Nishanth Chandran, Ramachandran Ramjee, Andreas Haberlen, Harmeet Singh, Abhishek Modi, Saikrishna Badrinarayanan

Technical Reports (CIS)

Today, enterprises collect large amounts of data and leverage the cloud to perform analytics over this data. Since the data is often sensitive, enterprises would prefer to keep it confidential and to hide it even from the cloud operator. Systems such as CryptDB and Monomi can accomplish this by operating mostly on encrypted data; however, these systems rely on expensive cryptographic techniques that limit performance in true “big data” scenarios that involve terabytes of data or more. This paper presents Seabed, a system that enables efficient analytics over large encrypted datasets. In contrast to previous systems, which rely on asymmetric ...


Loopy: Programmable And Formally Verified Loop Transformations, Kedar S. Namjoshi, Nimit Singhania Jul 2016

Loopy: Programmable And Formally Verified Loop Transformations, Kedar S. Namjoshi, Nimit Singhania

Technical Reports (CIS)

Abstract. This paper presents a system, Loopy, for programming loop transformations. Manual loop transformation can be tedious and errorprone, while fully automated methods do not guarantee improvements. Loopy takes a middle path: a programmer specifies a loop transformation at a high level, which is then carried out automatically by Loopy, and formally verified to guard against specification and implementation mistakes. Loopy’s notation offers considerable flexibility with assembling transformations, while automation and checking prevent errors. Loopy is implemented for the LLVM framework, building on a polyhedral compilation library. Experiments show substantial improvements over fully automated loop transformations, using simple and ...


Orca: Ordering-Free Regions For Consistency And Atomicity, Christian Delozier, Yuanfeng Peng, Ariel Eizenberg, Brandon Lucia, Joe Devietti Apr 2016

Orca: Ordering-Free Regions For Consistency And Atomicity, Christian Delozier, Yuanfeng Peng, Ariel Eizenberg, Brandon Lucia, Joe Devietti

Technical Reports (CIS)

Writing correct synchronization is one of the main difficulties of multithreaded programming. Incorrect synchronization causes many subtle concurrency errors such as data races and atomicity violations. Previous work has proposed stronger memory consistency models to rule out certain classes of concurrency bugs. However, these approaches are limited by a program’s original (and possibly incorrect) synchronization. In this work, we provide stronger guarantees than previous memory consistency models by punctuating atomicity only at ordering constructs like barriers, but not at lock operations. We describe the Ordering-free Regions for Consistency and Atomicity (ORCA) system which enforces atomicity at the granularity of ...


An Empirical Study Of Off-By-One Loop Mutation, M. S. Raunak, Christian Murphy, Bryan O'Haver Jul 2015

An Empirical Study Of Off-By-One Loop Mutation, M. S. Raunak, Christian Murphy, Bryan O'Haver

Technical Reports (CIS)

Context: Developing test cases that are measurably effective in finding faults in programs is a very challenging research problem. Mutation testing, a prominent technique developed to address this challenge, often becomes com- putationally too expensive for practical use due to the very large number of mutants that need to be analyzed. Objective: This paper evaluates the impact of One-by-one (OBO) loop mutation in reducing the cost of mutation analysis and investigates this technique's effectiveness in measuring the strength or weakness of test suites. Method: A set of Java and C programs have been used to generate both OBO and ...


Magiccarpet: Verified Detection And Recovery For Hardware-Based Exploits, Cynthia Sturton, Matthew Hicks, Samuel T. King, Jonathan M. Smith Mar 2015

Magiccarpet: Verified Detection And Recovery For Hardware-Based Exploits, Cynthia Sturton, Matthew Hicks, Samuel T. King, Jonathan M. Smith

Technical Reports (CIS)

Abstract—MAGICCARPET is a new approach to defending systems against exploitable processor bugs. MAGICCARPET uses hardware to detect violations of invariants involving security-critical processor state and uses firmware to correctly push software’s state past the violations. The invariants are specified at run time. MAGICCARPET focuses on dynamically validating updates to security-critical processor state. In this work, (1) we generate correctness proofs for both MAGICCARPET hardware and firmware; (2) we prove that processor state and events never violate our security invariants at runtime; and (3) we show that MAGICCARPET copes with hardware-based exploits discovered post-fabrication using a combination of verified ...


Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich Oct 2014

Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich

Technical Reports (CIS)

This paper presents the design of ZOMBIE, a dependently-typed programming language that uses an adaptation of a congruence closure algorithm for proof and type inference. This algorithm allows the type checker to automatically use equality assumptions from the context when reasoning about equality. Most dependently typed languages automatically use equalities that follow from -reduction during type checking; however, such reasoning is incompatible with congruence closure. In contrast, ZOMBIE does not use automatic -reduction because types may contain potentially diverging terms. Therefore ZOMBIE provides a unique opportunity to explore an alternative definition of equivalence in dependently typed language design. Our work ...


A Linear/Producer/Consumer Model Of Classical Linear Logic, Jennifer Paykin, Stephan A. Zdancewic Feb 2014

A Linear/Producer/Consumer Model Of Classical Linear Logic, Jennifer Paykin, Stephan A. Zdancewic

Technical Reports (CIS)

This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions that reflect the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into the category theory. The ...


Improving The Estimation Of Word Importance For News Multi-Document Summarization - Extended Technical Report, Kai Hong, Ani Nenkova Feb 2014

Improving The Estimation Of Word Importance For News Multi-Document Summarization - Extended Technical Report, Kai Hong, Ani Nenkova

Technical Reports (CIS)

In this paper, we propose a supervised model for ranking word importance that incorporates a rich set of features. Our model is superior to prior approaches for identifying words used in human summaries. Moreover we show that an extractive summarizer which includes our estimation of word importance results in summaries comparable with the state-of-the-art by automatic evaluation.


Maximization Of Non-Monotone Submodular Functions, Jennifer Gillenwater Jan 2014

Maximization Of Non-Monotone Submodular Functions, Jennifer Gillenwater

Technical Reports (CIS)

A litany of questions from a wide variety of scientific disciplines can be cast as non-monotone submodular maximization problems. Since this class of problems includes max-cut, it is NP-hard. Thus, general purpose algorithms for the class tend to be approximation algorithms. For unconstrained problem instances, one recent innovation in this vein includes an algorithm of Buchbinder et al. (2012) that guarantees a ½ - approximation to the maximum. Building on this, for problems subject to cardinality constraints, Buchbinderet al. (2014) o_er guarantees in the range [0:356; ½ + o(1)]. Earlier work has the best approximation factors for more complex constraints ...


Notes On Convex Sets, Polytopes, Polyhedra, Combinatorial Topology, Voronoi Diagrams And Delaunay Triangulations, Jean H. Gallier Nov 2013

Notes On Convex Sets, Polytopes, Polyhedra, Combinatorial Topology, Voronoi Diagrams And Delaunay Triangulations, Jean H. Gallier

Technical Reports (CIS)

Some basic mathematical tools such as convex sets, polytopes and combinatorial topology are used quite heavily in applied fields such as geometric modeling, meshing, computer vision, medical imaging and robotics. This report may be viewed as a tutorial and a set of notes on convex sets, polytopes, polyhedra, combinatorial topology, Voronoi Diagrams and Delaunay Triangulations. It is intended for a broad audience of mathematically inclined readers.

One of my (selfish!) motivations in writing these notes was to understand the concept of shelling and how it is used to prove the famous Euler-Poincare formula(Poincare, 1899) and the more recent Upper ...


Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich Nov 2013

Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich

Technical Reports (CIS)

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.


A Modal Specification Theory For Timing Variability, Andrew King, Oleg Sokolsky, Insup Lee Nov 2013

A Modal Specification Theory For Timing Variability, Andrew King, Oleg Sokolsky, Insup Lee

Technical Reports (CIS)

Modal specifications are classical formalisms that can be used to express the functional variability of systems; it is particularly useful for capturing the stepwise refinement of component-based design. However, the extension of such formalisms to real-time systems has not received adequate attention. In this paper, we propose a novel notion of time-parametric modal specifications to describe the timing as well as functional variability of real-time systems.We present a specification theory on modal refinement, property preservation and compositional reasoning. We also develop zone-graph based symbolic methods for the reachability analysis and modal refinement checking. We demonstrate the practical application of ...


Clifford Algebras, Clifford Groups, And A Generalization Of The Quaternions: The Pin And Spin Groups, Jean H. Gallier Nov 2013

Clifford Algebras, Clifford Groups, And A Generalization Of The Quaternions: The Pin And Spin Groups, Jean H. Gallier

Technical Reports (CIS)

One of the main goals of these notes is to explain how rotations in Rn are induced by the action of a certain group, Spin(n), on Rn, in a way that generalizes the action of the unit complex numbers, U(1), on R2, and the action of the unit quaternions, SU(2), on R3 (i.e., the action is denied in terms of multiplication in a larger algebra containing both the
group Spin(n) and R(n). The group Spin(n), called a spinor group, is defined as a certain subgroup of units of an algebra, Cln, the Clifford ...


Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino Jan 2013

Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino

Technical Reports (CIS)

Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, mega). Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can ...


Notes On Elementary Spectral Graph Theory Applications To Graph Clustering Using Normalized Cuts, Jean H. Gallier Jan 2013

Notes On Elementary Spectral Graph Theory Applications To Graph Clustering Using Normalized Cuts, Jean H. Gallier

Technical Reports (CIS)

These are notes on the method of normalized graph cuts and its applications to graph clustering. I provide a fairly thorough treatment of this deeply original method due to Shi and Malik, including complete proofs. I include the necessary background on graphs and graph Laplacians. I then explain in detail how the eigenvectors of the graph Laplacian can be used to draw a graph. This is an attractive application of graph Laplacians. The main thrust of this paper is the method of normalized cuts. I give a detailed account for K = 2 clusters, and also for K > 2 clusters, based ...


On The Coordinated Navigation Of Multiple Independent Disk-Shaped Robots, Cem Serkan Karagöz, H. Isil Bozma, Daniel E. Koditschek Jan 2003

On The Coordinated Navigation Of Multiple Independent Disk-Shaped Robots, Cem Serkan Karagöz, H. Isil Bozma, Daniel E. Koditschek

Technical Reports (CIS)

This paper addresses the coordinated navigation of multiple independently actuated disk-shaped robots - all placed within the same disk-shaped workspace. Assuming perfect sensing, shared centralized communications and computation, as well as perfect actuation, we encode complete information about the goal, obstacles and workspace boundary using an artificial potential function over the cross product space of the robots’ simultaneous configurations. The closed-loop dynamics governing the motion of each robot take the form of the appropriate projection of the gradient of this function. We show, with some reasonable restrictions on the allowable goal positions, that this function is an essential navigation function - a ...


Bracketing Guidelines For Treebank Ii Style Penn Treebank Project, Ann Bies, Mark Ferguson, Karen Katz, Robert Macintyre Jan 1995

Bracketing Guidelines For Treebank Ii Style Penn Treebank Project, Ann Bies, Mark Ferguson, Karen Katz, Robert Macintyre

Technical Reports (CIS)

No abstract provided.


Modeling And Animating Human Figures In A Cad Environment, Norman I. Badler Dec 1986

Modeling And Animating Human Figures In A Cad Environment, Norman I. Badler

Technical Reports (CIS)

With the widespread acceptance of three-dimensional modeling techniques, high-speed hardware, and relatively low-cost computation, modeling and animating one or more human figures for the purposes of design assessment, human factors, task simulation, and human movement understanding has become feasible outside the animation production house environment. This tutorial will address the state-of-the-art in human figure geometric modeling, figure positioning, figure animation, and task simulation.


The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom Sep 1985

The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom

Technical Reports (CIS)

We briefly survey the major thrusts of computer graphics activities, examining trends and topics rather than offering a comprehensive survey of all that is happening. The directions of professional activities, hardware, software, and algorithms are outlined. Within hardware we examine workstations, personal graphics systems, high performance systems, and low level VLSI chips; within software, standards and interactive system design; within algorithms, visible surface rendering and shading, three-dimensional modeling techniques, and animation.

Note: This paper was presented at Eurographics'84 in Copenhagen, Denmark.


Appendices - Parametric Keyframe Interpolation Incorporating Kinetic Adjustment And Phrasing Control, Scott N. Steketee, Norman I. Badler Jul 1985

Appendices - Parametric Keyframe Interpolation Incorporating Kinetic Adjustment And Phrasing Control, Scott N. Steketee, Norman I. Badler

Technical Reports (CIS)

These are the unpublished appendices for the paper entitled, "Parametric Keyframe Interpolation Incorporating Kinetic Adjustment and Phrasing Control."


Guide: Graphical User Interfaced Development Environment, Tamar E. Granor, Norman I. Badler May 1985

Guide: Graphical User Interfaced Development Environment, Tamar E. Granor, Norman I. Badler

Technical Reports (CIS)

GUIDE is an interactive graphical system for designing and generating graphical user interfaces. It provides flexibility to the system designer while minimizing the amount of code which the designer must write. The GUIDE methodology includes the notions of "tool," "task," and "context." GUIDE encourages designers to tailor their systems to individual users by inclusion of "user profiles," allowing different control paths based on the user's characteristics. GUIDE also provides a method for invoking application routines with parameters. Parameters may be based on user inputs and are computed at invocation time. Help messages are created along with the objects to ...


Tempus: A System For The Design And Simulation Of Human Figures In A Task-Oriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro Brotman Jan 1985

Tempus: A System For The Design And Simulation Of Human Figures In A Task-Oriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro Brotman

Technical Reports (CIS)

A system called TEMPUS is outlined which is being developed to simulate graphically the task-oriented activities of several human agents in a three-dimensional environment. TEMPUS is a task simulation facility for the evaluation of complex workstations vis-a-vis the normal and emergency procedures they are intended to support and the types and number of individuals who must carry them out. TEMPUS allows a user to interactively:

  • Create on or more human figures which are correctly scaled according to a specific population, or which meet certain size constraints.
  • View the human figure in any of several graphical modes: stick figure, line or ...


Local Matching Of Surfaces Using Critical Points, Gerald Radack, Norman I. Badler May 1984

Local Matching Of Surfaces Using Critical Points, Gerald Radack, Norman I. Badler

Technical Reports (CIS)

The local matching problem on surfaces is: Given a pair of oriented surfaces in 3-space, find subsurfaces that are identical or complementary in shape. A heuristic method is presented for local matching that is intended for use on complex curved surfaces (rather than such surfaces as as cubes and cylinders).

The method proceeds as follows: (1) Find a small set of points-called "critical points" -on the two surfaces with the property that if p is a critical point and p matches q, then q is also a critical point. The critical points are taken to be local extrema of either ...


Generating Shadows With An Umbra And Penumbra, Lynne Shapiro, Norman I. Badler Jan 1984

Generating Shadows With An Umbra And Penumbra, Lynne Shapiro, Norman I. Badler

Technical Reports (CIS)

An algorithm for generating shadows with an umbra and penumbra due to distributed light sources is presented. The method used is based on the inclusion of the shadow volumes in the object data processed by a depth-buffer visible surface computation. The standard depth-buffer data structure is modified to allow the handling of shadows with a depth-buffer hidden surface algorithm. The algorithm involves breaking the light source up into a set of point sources and superimposing the shadows generated by each point source to obtain the final shadow.


The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom Jan 1984

The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom

Technical Reports (CIS)

We briefly survey the major thrusts of computer graphics activities, examining trends and topics rather than offering a comprehensive survey of all that is happening. The directions of professional activities, hardware, software, and algorithms are outlined. Within hardware we examine workstations, personal graphics systems, high performance systems, and low level VLSI chips; within software, standards and interactive system design; within algorithms, visible surface rendering and shading, three-dimensional modeling techniques, and animation.


Outline Of A Calculus Of Type Subsumption, Hassan Aït-Kaci Aug 1983

Outline Of A Calculus Of Type Subsumption, Hassan Aït-Kaci

Technical Reports (CIS)

This paper is a brief analysis of the notion of syntactic representation of types followed by a proposal of a formal calculus of type subsumption. The idea which is developed centers on the concept of indexed term, an extension of the definition of algebraic terms relaxing the fixed arity and fixed indexing constraints, and which allows term symbols to have some pre-order structure. It is shown that the structure on the set of symbols can be "homomorphically" extended to indexed terms to what is defined to be a subsumption ordering. Furthermore, when symbols have a lattice structure, this structure extends ...


Tempus: A System For The Design And Simulation Of Human Figures In A Task-Oriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro, Carolyn Brown Jan 1983

Tempus: A System For The Design And Simulation Of Human Figures In A Task-Oriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro, Carolyn Brown

Technical Reports (CIS)

A system called TEMPUS is outlined which is being developed to simulate graphically the task-oriented activities of several human agents in a three-dimensional environment. TEMPUS is a task simulation facility for the evaluation of complex workstations vis-a-vis the normal and emergency procedures they are intended to support and the types and number of individuals who must carry them out. TEMPUS allows a user to interactively:

* Create one or more human figures which are correctly scaled according to a specific population, or which meet certain size constraints.

* View the human figure in any of several graphical modes: stick figure, line or ...