arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Limor Fix

20 papers · 1996–2016

1996: 11997: 01998: 11999: 02000: 02001: 12002: 22003: 02004: 12005: 32006: 42007: 32008: 12009: 02010: 02011: 02012: 02013: 12014: 02015: 02016: 2
1996peak 4 in 20062016

Frequent co-authors

Papers

showing 1–20 of 20 RSS

Scheduling threads for constructive cache sharing on CMPs

Shimin Chen, Phillip B. Gibbons, Michael A. Kozuch +8 more

Hardware and Architecture · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · · cited 167× · DOI ↗ · more like this ·

In chip multiprocessors (CMPs), limiting the number of offchip cache misses is crucial for good performance. Many multithreaded programs provide opportunities for constructive cache sharing, in which concurrently scheduled threads share a largely overlapping working set. In this paper, we compare the performance of two state-of-the-art schedulers proposed for fine-grained multithreaded programs: Parallel Depth First (PDF), which is specifically designed for constructive cache sharing, and Work Stealing (WS), which is a more traditional design. Our experimental results indicate that PDF scheduling yields a 1.3--1.6X performance improvement relative to WS for several fine-grain parallel benchmarks on projected future CMP configurations; we also report several issues that may limit the advantage of PDF in certain applications. These results also indicate that PDF more effectively utilizes…

Log-based architectures for general-purpose monitoring of deployed code

Shimin Chen, Babak Falsafi, Phillip B. Gibbons +8 more

Hardware and Architecture · The HKU Scholars Hub (University of Hong Kong) · · cited 72× · DOI ↗ · more like this ·

Runtime monitoring tools are invaluable for detecting various types of bugs, in both sequential and multi-threaded programs. However, these tools often slow down the monitored program by an order of magnitude or more [4], implying that the tools are ill-suited for always-on monitoring of deployed code. Fortunately, the emergence of chip multiprocessors as a dominant computing platform means that resources are available on-chip to assist in monitoring tasks. In this brief note, we advocate Log-Based Architectures (LBA) that exploit such on-chip resources in order to dramatically reduce the overhead of runtime program monitoring. Specifically, we propose adding hardware support for logging a main program's trace and delivering it to another (otherwise idle) processing core for inspection. A life-guard program running on this other core executes the desired monitoring task.

Systems Computing Challenges in the Internet of Things

Rajeev Alur, Emery Berger, Ann W. Drobnis +10 more

cs.CY · · cited 49× · arXiv ↗ · more like this ·

A recent McKinsey report estimates the economic impact of the Internet of Things (IoT) to be between $3.9 to $11 trillion dollars by 20251 . IoT has the potential to have a profound impact on our daily lives, including technologies for the home, for health, for transportation, and for managing our natural resources. The Internet was largely driven by information and ideas generated by people, but advances in sensing and hardware have enabled computers to more easily observe the physical world. Coupling this additional layer of information with advances in machine learning brings dramatic new capabilities including the ability to capture and process tremendous amounts of data; to predict behaviors, activities, and the future in uncanny ways; and to manipulate the physical world in response. This trend will fundamentally change how people interact with physical objects and the…

A hybrid verification approach

Scott Hazelhurst, Osnat Weissberg, Gila Kamhi +1 more

Computational Theory and Mathematics · Proceedings - ACM IEEE Design Automation Conference · · cited 36× · DOI ↗ · more like this ·

One method of handling the computational complexity of the verification process is to combine the strengths of different approaches. We propose a hybrid verification technology combining symbolic trajectory evaluation with either symbolic model checking or SAT-based model checking. This reduces significantly the cost (both human and computing) of verifying circuits with complex initialisation, as well as simplifying proof development by enhancing verification productivity. The approach has been tested on current Intel designs.

SAT-based Induction for Temporal Safety Properties

Roy Armoni, Limor Fix, Ranan Fraer +3 more

Computational Theory and Mathematics · Electronic Notes in Theoretical Computer Science · · cited 30× · DOI ↗ · more like this ·

The work presented in this paper addresses the challenge of fully verifying complex temporal properties on large RTL designs. Windowed induction has been proposed by Sheeran, Singh, and Stalmarck as a technique augmenting Bounded Model Checking for unbounded verification of safety properties. While induction proved to be quite effective for combinational properties, the case of temporal properties was not handled by previously known methods. We introduce explicit induction, a new induction scheme targeted to temporal properties, and to interactive development of inductive proofs. The innovative idea in explicit induction is to make the induction scheme an explicit part of the specification, where it can be easily controlled, using a highly expressive language like ForSpec. We show how explicit induction was implemented with minor modifications in the ForSpec compiler and in Thunder, a…

Formal methods for analyzing the completeness of an assertion suite against a high-level fault model

Sayanlan Das, Ansuman Banerjee, Prasenjit Basu +4 more

Computational Theory and Mathematics · · cited 22× · DOI ↗ · more like this ·

One of the emerging challenges in formal property verification (FPV) technology is the problem of deciding whether sufficient properties have been written to cover the design intent. Existing literature on FPV coverage does not solve this problem adequately, since they primarily analyze the coverage of a specification against a given implementation. On the other hand, we consider the task of determining the coverage of a formal specification against a high-level fault model that is independent of any specific implementation. We show that such a coverage analysis discovers behavioral gaps in the specification and prompts the design architect to add more properties to close the behavioral gaps. Our results establish that the coverage analysis task at this level is computationally complex, but it is possible to obtain a conservative estimate of the coverage at low cost.

Verification of temporal properties

Limor Fix

Computational Theory and Mathematics · Journal of Logic and Computation · · cited 17× · DOI ↗ · more like this ·

The paper presents a relatively complete deductive system for proving branching time temporal properties of reactive programs. No deductive system for verifying branching time temporal properties has been presented before. Our deductive system enjoys the following advantages. First, given a well-formed specification there is no need to translate it into a normal-form specification since the system can handle any well-formed specification. Second, given a specification to be verified, the proof rule to be applied is easily determined according to the top level operator of the specification. Third, the system reduces temporal verification to assertional reasoning rather than to temporal reasoning.

Design-Intent Coverage—A New Paradigm for Formal Property Verification

Parthiba Basu, Susobhan Das, Ansuman Banerjee +5 more

Computational Theory and Mathematics · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · · cited 16× · DOI ↗ · more like this ·

It is essential to formally ascertain whether the register-transfer level (RTL) validation effort effectively guarantees the correctness with respect to the design's architectural intent. The design's architectural intent can be expressed in formal properties. However, due to the capacity limitations of formal verification, these architectural properties cannot be directly verified on the RTL. As a result, a set of lower level RTL properties are developed and verified against the RTL modules. In a top-down design approach, the architect would ideally like to formally guarantee the coverage of the architectural intent at the time of creating the specifications for the component RTL modules (that is, before they are passed to the designers for implementation). In this paper, the authors present: 1) a method for checking whether the RTL properties are covering the architectural properties…

Adaptive variable reordering for symbolic model checking

Gila Kamhi, Limor Fix

Computational Theory and Mathematics · · cited 16× · DOI ↗ · more like this ·

Article Free Access Share on Adaptive variable reordering for symbolic model checking Authors: Gila Kamhi Future CAD Technologies, Intel Israel Ltd., P.O. BOX 1659, Haifa, Israel Future CAD Technologies, Intel Israel Ltd., P.O. BOX 1659, Haifa, IsraelView Profile , Limor Fix Future CAD Technologies, Intel Israel Ltd., P.O. BOX 1659, Haifa, Israel Future CAD Technologies, Intel Israel Ltd., P.O. BOX 1659, Haifa, IsraelView Profile Authors Info & Claims ICCAD '98: Proceedings of the 1998 IEEE/ACM international conference on Computer-aided designNovember 1998 Pages 359–365https://doi.org/10.1145/288548.289054Published:01 November 1998Publication History 12citation224DownloadsMetricsTotal Citations12Total Downloads224Last 12 Months10Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that…

Formal verification coverage: computing the coverage gap between temporal specifications

Arindam Das, Parthiba Basu, Ansuman Banerjee +5 more

Computational Theory and Mathematics · · cited 13× · DOI ↗ · more like this ·

Existing methods for formal verification coverage compare a given specification with a given implementation, and evaluate the coverage gap in terms of quantitative metrics. We consider a new problem, namely to compare two formal temporal specifications and to find a set of additional temporal properties that close the coverage gap between the two specifications. In this paper we present: (1) the problem definition and motivation, (2) a methodology for computing the coverage gap between specifications, and (3) a methodology for representing the coverage gap as a collection of temporal properties that preserve the syntactic structure of the target specification.

Parallel depth first vs. work stealing schedulers on CMP architectures

Vasileios Liaskovitis, Shimin Chen, Phillip B. Gibbons +8 more

Hardware and Architecture · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · · cited 5× · DOI ↗ · more like this ·

In chip multiprocessors (CMPs), limiting the number of off-chip cache misses is crucial for good performance. Many multithreaded programs provide opportunities for constructive cache sharing, in which concurrently scheduled threads share a largely overlapping working set. In this brief announcement, we highlight our ongoing study [4] comparing the performance of two schedulers designed for fine-grained multithreaded programs: Parallel Depth First (PDF) [2], which is designed for constructive sharing, and Work Stealing (WS) [3], which takes a more traditional approach.Overview of schedulers. In PDF, processing cores are allocated ready-to-execute program tasks such that higher scheduling priority is given to those tasks the sequential program would have executed earlier. As a result, PDF tends to co-schedule threads in a way that tracks the sequential execution. Hence, the aggregate…

Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting

Ranan Fraer, Gila Kamhi, Limor Fix +1 more

Software · Electronic Notes in Theoretical Computer Science · · cited 5× · DOI ↗ · more like this ·

We propose a methodology to evaluate a rich set of BDD subsetting heuristics with respect to bug hunting and apply it to a set of real-life Intel designs. Our results illustrate that the evaluation metrics used to rate these heuristics in previous work were not tuned for bug-finding efficiency, which we believe is the major criterion that the heuristics need to meet.

VERIFYING VERY LARGE INDUSTRIAL CIRCUITS USING 100 PROCESSES AND BEYOND

Limor Fix, Orna Grümberg, Amnon Heyman +2 more

Computational Theory and Mathematics · International Journal of Foundations of Computer Science · · cited 4× · DOI ↗ · more like this ·

Recent advances in scheduling and networking have paved the way for efficient exploitation of large-scale distributed computing platforms such as computational grids and huge clusters. Such infrastructures hold great promise for the highly resource-demanding task of verifying and checking large models, given that model checkers would be designed with a high degree of scalability and flexibility in mind. In this paper we focus on the mechanisms required to execute a high-performance, distributed, symbolic model checker on top of a large-scale distributed environment. We develop a hybrid algorithm for slicing the state space and dynamically distribute the work among the worker processes. We show that the new approach is faster, more effective, and thus much more scalable than previous slicing algorithms. We then present a checkpoint-restart module that has very low overhead. This module…

Deeper Bound in BMC by Combining Constant Propagation and Abstraction

Roy Armoni, Limor Fix, Ranan Fraer +4 more

Computational Theory and Mathematics · · cited 4× · DOI ↗ · more like this ·

The most successful technologies for automatic verification of large industrial circuits are bounded model checking, abstraction, and iterative refinement. Previous work has demonstrated the ability to verify circuits with thousands of state elements achieving bounds of at most a couple of hundreds. In this paper we present several novel techniques for abstraction-based bounded model checking. Specifically, we introduce a constant-propagation technique to simplify the formulas submitted to the CNF SAT solver; we present a new proof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate our ability to handle circuit with several thousands state elements reaching bounds nearing 1,000.

Brief announcement: Parallel depth first vs. work stealing schedulers on CMP architectures

Vasileios Liaskovitis, Shimin Chen, Phillip B. Gibbons +8 more

Hardware and Architecture · · cited 1× · OpenAlex ↗ · more like this ·

In chip multiprocessors (CMPs), limiting the number of off-chip cache misses is crucial for good performance. Many multithreaded programs provide opportunities for constructive cache sharing, in which concurrently scheduled threads share a largely overlapping working set. In this brief announcement, we highlight our ongoing study [4] comparing the performance of two schedulers designed for fine-grained multithreaded programs: Parallel Depth First (PDF) [2], which is designed for constructive sharing, and Work Stealing (WS) [3], which takes a more traditional approach. Overview of schedulers. In PDF, processing cores are allocated ready-to-execute program tasks such that higher scheduling priority is given to those tasks the sequential program would have executed earlier. As a result, PDF tends to

Formal verification methods

David L. Dill, Nate James, Shishpal Rawat +6 more

Artificial Intelligence · Proceedings - ACM IEEE Design Automation Conference · · cited 1× · DOI ↗ · more like this ·

Do formal verification tools and methodologies require a drastic overhaul to move beyond equivalence checking? Equivalence checking catches errors in synthesis and local hand-modifications to designs. However, powerful formal verification technologies are emerging to combat "behavioral" errors, which represent today's biggest verification problems. Nonetheless, formal verification experts are split on how formal tools should adapt to this challenge. Some of our panelists feel that designers can sufficiently benefit from new formal verification technologies by making incremental changes to current methodologies. Others, however, argue that major changes are required to reap meaningful benefits from these new technologies. Just how much change is enough, what is the capacity of our current tools and what is limiting the full deployment of FV technology.Our panel of experts, consisting of…

3C-1 Deeper Bound in BMC by Combining Constant Propagation and Abstraction

Roy Armoni, Limor Fix, Ranan Fraer +4 more

Computational Theory and Mathematics · · cited 0× · OpenAlex ↗ · more like this ·

Abstract The most successful technologies for automatic verification of large industrial circuits are bounded model checking, abstraction, and iterative refinement. Previous work has demonstrated the ability to verify circuits with thousands of state elements achieving bounds of at most a couple of hundreds. In this paper we present several novel techniques for abstraction-based bounded model checking. Specifically, we introduce a constant-propagation technique to simplify the formulas submitted to the CNF SAT solver; we present a new proof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate our ability to handle circuit with several thousands state elements reaching bounds nearing 1,000. I.

BMC 2004 Preliminary Version SAT-based Induction for Temporal Safety Properties

Roy Armoni A, Limor Fix A, Ranan Fraer A +3 more

Computational Theory and Mathematics · · cited 0× · OpenAlex ↗ · more like this ·

The work presented in this paper addresses the challenge of fully verifying complex temporal properties on large RTL designs. Windowed induction has been proposed by Sheeran, Singh, and Stalmarck as a technique augmenting Bounded Model Checking for unbounded verification of safety properties. While induction proved to be quite effective for combinational properties, the case of temporal properties was not handled by previously known methods. We introduce explicit induction, a new induction scheme targeted to temporal properties, and to interactive development of inductive proofs. The innovative idea in explicit induction is to make the induction scheme an explicit part of the specification, where it can be easily controlled, using a highly expressive language like ForSpec. We show how explicit induction was implemented with minor modifications in the ForSpec compiler and in Thunder, a…

The Future of Computing Research: Industry-Academic Collaborations

Nady Boules, Khari Douglas, Stuart Feldman +8 more

cs.CY · · arXiv ↗ · more like this ·

IT-driven innovation is an enormous factor in the worldwide economic leadership of the United States. It is larger than finance, construction, or transportation, and it employs nearly 6% of the US workforce. The top three companies, as measured by market capitalization, are IT companies - Apple, Google (now Alphabet), and Microsoft. Facebook, a relatively recent entry in the top 10 list by market capitalization has surpassed Walmart, the nation's largest retailer, and the largest employer in the world. The net income of just the top three exceeds $80 billion - roughly 100 times the total budget of the NSF CISE directorate which funds 87% of computing research. In short, the direct return on federal research investments in IT research has been enormously profitable to the nation. The IT industry ecosystem is also evolving. The time from conception to market of successful products has…