shengyushen's academic research

CCS'03: Randomized instruction set emulation to disrupt binary code injection attacks

2012-02-19T21:59:00.001+08:00

This paper is very similar to the previous one, except that is store the original program on disk, and randomize it while loading it into memory.

And its key is very long, may be as long as the program.

CCS'03:Countering Code-Injection Attacks With Instruction-Set Randomization

2012-02-19T21:23:00.001+08:00

This paper proposes an approach to counter the code injection attacks. It stores key for de-randomizing the randomized program. When the OS tries to schedule the program to run, it will load this key into a write-only register in CPU, and the CPU will de-randomize the input instruction stream before the CPU actually process it.

ASPLOS'10:Speculative Parallelization Using Software Multi-threaded Transactions

2012-02-18T20:37:00.007+08:00

This paper proposes a software transaction memory system that can maintain automic across multiple thread.

ASPLOS'10: COMPASS: A Programmable Data Prefetcher Using Idle GPU Shaders

2012-02-18T20:37:00.005+08:00

This paper proposes to use the GPU as a programable unit to run a GPU program that help prefetching the data for CPU.

ASPLOS'10: Dynamically Replicated Memory: Building Reliable Systems from Nanoscale Resistive Memories

2012-02-18T20:37:00.003+08:00

This paper proposes to add another level of page table that maps the physical address to real address in PCM. This mapping can map a physical page to two PCM page that have different stuck-at fault locations. In this way, the PCM pages can still be used instead of discarded.

ASPLOS'10: Inter-Core Cooperative TLB Prefetchers for Chip Multiprocessors

2012-02-18T20:37:00.001+08:00

This paper proposes mechanism that exploits the relation between the TLBs of different cores in CMP.

ASPLOS'10:Dynamic Filtering: Multi-Purpose Architecture Support for Language Runtime Systems

2012-02-18T20:31:00.001+08:00

This paper proposes a hardware mechanism and instrutions to detect the rare cases that checked repeatedly in STM and GC for some address patten.

ASPLOS'10: Flexible Architectural Support for Fine-Grain Scheduling

2012-02-12T19:45:00.005+08:00

Fine-grain scheduling, which schedule small threads with only thousands of instructions, requires exchanging huge amount of information across multi-level of cache and memory, which leads to about 100 cycles for every scheduling that is unacceptable for such small threads.On the other hand, purely hardware scheduler is not flexiable enough to deploy multiple scheduling algorithm. So this paper proposes a flexiable message exchange mechnism that can be used by software scheduler to avoid the need of crossing multiple level of caches, while preserve the flexiability.

ISCA'10: Necromancer: Enhancing System Throughput by Animating Dead Cores

2012-02-12T19:45:00.003+08:00

In manufactoring test, any core that can not pass will be disabled, but they are most correct with only minor bugs. So this paper use them to run ahead and direct a simpler core with useful information, such as branch destination and cache prefetch, thus lead to bettern performance on the simpler core.

ISCA'10: Elastic Cooperative Caching: An Autonomous Dynamically Adaptive Memory Hierarchy for Chip Multiprocessors

2012-02-12T19:45:00.001+08:00

This paper proposes an interesting cache design, in which every cache is divided into private and shared part. The private part is only for the attached core, while the shared part can be alloced to other core, leading to a much larger private cache for other cores.

ISCA'10 : ynamic Warp Subdivision for Integrated Branch and Memory Divergence Tolerance

2012-02-12T19:44:00.004+08:00

This paper proposes to divide the SIMD lanes into two seperate sets on lane Divergence caused by different in branch or memory latency. And then these sets can be executed as threads interleaved.

ISCA'10 : A Case for FAME: FPGA Architecture Model Execution This paper surveies many types of FPGA emulation system.

2012-02-12T19:44:00.002+08:00

Direct FAME blow the rtl directly into FPGA, which is currently used by use.
Decoupled FAME use many cycle to simulate a single cycle of a complex device, such as the multi-port reg file.
Multithread use a single pipeline and many state set to simulate many different copy, such as cores.

ISCA'10: Translation Caching: Skip, Don’t Walk (the Page Table)

2012-02-12T19:44:00.000+08:00

Every TLB miss may require several dram access, each for a page table level.

MMU caches are used to store those page entries like data cache.

There are many varaints, such as unified one that store all level of entries in one cache, or seperated one that store entries of each level in different cache. Another varaint is that Page Table Cache that indexed by the physical address of the entries, which shows how to find the entries, or translation cache that store the translation result, thus make it indexed by virtual address.

ISCA'10: Sentry: Light-Weight Auxiliary Memory Access Control

2012-01-25T21:58:00.000+08:00

This paper proposes a finer grain memory protection mechanism that work at cache line level. It reside on the L1 cache 1 miss path, thus prevent it from slow down the processor pipeline and consume power very cycle.

ISCA'11 : The Role of Optics in Future High Radix Switch Design

2012-01-24T20:33:00.002+08:00

This paper shows some dark future of the electrical switcher, and proposes to use optical switcher.

We need to further reread of its content when we need optical serdes.

ISCA'11: Dark Silicon and the End of Multicore Scaling

2012-01-24T20:09:00.002+08:00

This paper presents a dark future of the multi core methodology, that it will end within 9 years due to the power and utilization wall.

ISCA'11 : SpecTLB: A Mechanism for Speculative Address Translation

2012-01-24T19:38:00.000+08:00

This paper proposes to parallel walking the page table and predicate the address translation result with interpolant, such that the translation latency can be hidden.

ISCA'11 : A Case for Globally Shared-Medium On-Chip Interconnect

2012-01-24T12:20:00.000+08:00

This paper presents a transmission line link design with standard CMOS implementation, at 26.4Gb/s. It is very impressive and we may need to refer to it latter.

But the diff wires are also similar to what I seen before in serdes reference clocks, can I use them ?

ISCA'11 : Releasing Efficient Beta Cores to Market Early

2012-01-18T20:12:00.001+08:00

This paper is very interesting that it can run a simple and slow but correct core with a complex, fast but buggy core together.

They check each other, if not match, the simple core is invoked.

ISCA'11 : FlexBulk: Intelligently Forming Atomic Blocks in Blocked-Execution Multiprocessors to Minimize Squashes

2012-01-18T19:25:00.001+08:00

Blocked-execution processor continuously run atomic blocks of instructions — also called Chunks. Larger chunk may lead to frequently contention, and lost performance.

This paper proposes an automatic algorithm to remove the contention.

ISCA'11 : OUTRIDER: Efficient Memory Latency Tolerance with Decoupled Strands

2012-01-17T21:09:00.002+08:00

This paper uses compiler to separate the instruction stream into several strands, some of them are memory accessing, others are memory consuming. Thus torelants long memory latency without huge hardware overhead like OOO.

ISCA'11: Increasing the Effectiveness of Directory Caches by Deactivating Coherence for Private Memory Blocks

2012-01-17T20:48:00.003+08:00

This paper proposes to dynamically detect the memory that can only be accessed by a core, and prevent them from being coherented.

ISCA'11 : FabScalar: Composing Synthesizable RTL Designs of Arbitrary Cores within a Canonical Superscalar Template

2012-01-17T20:48:00.001+08:00

This paper proposes to generate superscalar processor from templates and stages with different width and depth.

ISCA'11: CRIB: Consolidated Rename, Issue, and Bypass

2012-01-17T20:47:00.001+08:00

Conventional high-performance processors use complex logic structure to deal with register rename, instruction schedule and so on jobs, only to make effecently use of heavily pipelined ALU and memory ports. This leads to huge dynamic power consumption.

This paper proposes a processor with lots of simple computation components-- CRIB, and make the computation happen in place instead of been scheduled by complex logic.

MICRO'11: Parallel Application Memory Scheduling

2011-12-25T17:35:00.002+08:00

This paper proposes to use run time system and compiler to find out the most contended lock and then the set of threads that may hold this lock, such that these threads may be prioritized in accessing memory.

For the barrier mechanism, a similar approach is also proposed.

FMCAD'11: Effective Word-Level Interpolation for Software Verification

2011-12-24T11:23:00.001+08:00

This paper proposes a novel approach to generate interpolant for BV using a layered structure, which includes 4 layers: the bit blasting , EUF, Equality Substitution

and linear arithmetic.

FMCAD'11: IC3: Where Monolithic and Incremental Meet

2011-12-24T11:17:00.001+08:00

The authors combines their incremental approach with old monolithic approach that overapproximates the reachability on longer and longer state sequences.

ASPLOS'10: Conservation Cores: Reducing the Energy of Mature Computations

2011-12-23T20:37:00.002+08:00

The dark silicon problem is attacked by this paper again. It states that with the silicon process advancement, the number of devices will double every generation, but the power budget remain unchanged, while the voltage and threshold voltage remain unchanged.

So the percentage of devices that can work at full speed will reduced from a generation to the next. So this paper proposes to synthesize specialized cores to run those hot code segments.

HPCA'10: Aérgia: Exploiting Packet Latency Slack in On-Chip Networks

2011-12-23T19:50:00.002+08:00

This paper proposes to use slack, the number of cycle that a package can be delayed without affecting the NOC performance, to arbitrate which package in contention should be forwarded.

And this paper also proposes approaches to approximate the slack by correlate it with i) the number of precedence L2 cache miss package ii) whether the package is itself a L2 miss and iii) the hop of this package.

HPCA'03 : Runahead Execution: An Alternative to Very Large Instruction Windows for Out-of-order Processors

2011-12-22T20:42:00.002+08:00

It mentions a very interesting technique, when the instruction window is blocked by a long run instruction, such as a memory access, the processor will check point current state and turn to a runahead mode, in which the processor run all following instructions but not commit their result.

When the long run instruction return back, the processor will return to the check pointed state and rerun all following instructions.

This technique can make all the data referred by following instructions to be fetched into cache before they are needed.

OSDI'10: FlexSC: Flexible System Call Scheduling with Exception-Less System Calls

2011-12-14T11:23:00.002+08:00

Current synchronous system call can evict large amount of cache and TLB. So frequently calling system calls will damage the performance.

This paper proposes to use an agent to hold all system call request, and halt the calling process or thread. When a certain number of calls are waiting or all process/threads are halting, then switch to the kernel mode to process all requests.

MICRO'11: Q S C ORES: Trading Dark Silicon for Scalable Energy Efficiency with Quasi-Specific Cores

2011-12-02T17:44:00.002+08:00

This paper analysizes the program benchmarks to find out hot fragment that are executed frequently, and then find out their common flow graph. And the use these commoness to synthesize new specialized core and integrated them with a general purpose processor.

MICRO'11: Manager-Client Pairing: A Framework for Implementing Coherence Hierarchies

2011-12-02T13:10:00.002+08:00

This paper proposes a hierarchical framework for cache coherent protocol, such that it can be designed in a multi-layer way.

Thus, this approach can avoid the design of a global single layer protocol that is neither salable nor power efficient.

MICRO'11:PACMan: Prefetch-Aware Cache Management for High Performance Caching

2011-12-02T13:06:00.001+08:00

This paper proposes a novel cache that knows the existence of prefetch, and deal it in a different way than normal data request.

MICRO'11:Idempotent Processor Architecture

2011-12-01T19:53:00.002+08:00

This paper proposes to use compiler to construct Idempotent region, a list of instructions that can reexecute again without obtaining different results.

And it also proposes a hardware structure that can execute such code. In this way, it can handle mispredication and exception cheaply.

MICRO'11: Architectural Support for Secure Virtualization under a Vulnerable Hypervisor

2011-11-30T20:04:00.002+08:00

To prevent the hypervisor from reading the guest VM's memory, this paper proposes hardware mechanism to hide the VM's status and memory owner mapping table from the hypervisor.

The hypervisor can still access these VM's private information be calling this novel hardware.

MICRO'11: Towards the Ideal On-chip Fabric for 1-to-Many and Many-to-1 Communication

2011-11-30T19:00:00.002+08:00

This paper proposes a NOC that support 1-M broadcast/multicasr and M-1 aggregation.

For 1-M, it can balance the usage of X and Y links.It also use matrix-like crossbar with tri-state driver to easy the layout and reduce power. It also reduce the traditional 3 stages pipeline to 1 cycle by sending the advance request before sending flit, such that the next router can perform arbitration before the flit actually arrive.

To aggregate the ACK messages, every ACK message arrive first will become the master at that router, and then each arriving ACK will be merged with the master by adding its ACK number to master's. After a predefined time, no matter whether the master had aggregate all ACKs, it will be send to upper stream router.

CAV'11: Linear Completeness Thresholds for Bounded Model Checking

2011-11-27T15:52:00.002+08:00

This paper find a set of LTL formulas that contains only F operator, is cliquey. That is, such formulas's corresponding Buchi automata's each SCC have bidirection edge between every two edges.

So when produced with a kripke structure M with recurence diameter rd, the product machine's diameter is a linear function of rd.

This paper also give an algorithm to computer an even tighter approximation of the product machine's diameter.

CAV'11: Interactive Synthesis of Code Snippets

2011-11-25T19:26:00.000+08:00

This paper improves PLDI'05 paper "Jungloid mining: helping to navigate the API jungle" by supporting parametric type that can lead to multiple ground type.

CAV'11: A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification

2011-11-25T19:10:00.001+08:00

The manipulation of seperation logics typically requires the unfolding of disjunctive predicates which may lead to expensive proof search.

This paper proposes to rule out invalid instances of predicates before unfolding, by propagating hidden properties to prune infeasible disjuncts.

CAV'10: Smoothing a Program Soundly and Robustly

2011-11-24T21:21:00.002+08:00

Based on previous work in "Smooth interpretation" PLDI'10, this paper propose three correctness requirements that make sure smoothing approach can be correctly applied.

1 soundness: general smoothing problem is undecidable, so an approximation is needed, which computes an k-dimension interval <{l_1,u_i},...,{l_k,u_k}> for each input. The soundness requirement is that the output ideal smooth function should be in this interval.

2 robustness: the resulting smooth function must have derivations of all order.

3 β-robustness: partial derivative is bounded by a function linear in x and β.A large number of numerical search routines work by sampling the input space under the expectation that the derivative around each sample point is well defined.

PLDI'10: Smooth interpretation

2011-11-24T16:54:00.003+08:00

In digital signal processing, there is Gaussian smoothing technology that can remove the noise of a signal by computing the convolution of the signal and Gaussian function.

This paper proposes to do the same on a simple imperative program that contains while loop, if statement, assign statement and Boolean/floating expression. This simple syntax seems somewhat like fortran.

This paper first perform symbolic simulation on this program to obtain its denotational semantics. And then take the convolution of this semantics and N(x,β), a joint density function of k independent normal variables, each with mean 0 and standard deviation β.

The resulting convolution will always be smooth, and the higher β, the smoother the convolution.

Thus, this smoothed program can be analysized by numerical optimization techniques. This paper uses technology in finding optimal parameter value of PID controller in physical-cyber system.

CAV'11: Quantitative Synthesis for Concurrent Programs

2011-11-24T15:24:00.002+08:00

This paper construct the product machine of the environment, the scheduler, the performance model and the partial program. The partial program contains some unspecified predicates that need to be inferred by the algorithm.

And then it is reduced to 2-player game with probabilistic transitions.

The most interesting thing to me is the probabilistic transition that computes a distribution on the next state set.

CAV'11: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications

2011-11-23T17:36:00.002+08:00

This paper first mentions some concepts that are not familiar to me:

1 Universal reduction : all universal qualified variables at the inner most layer can be removed

2 Q-resolution : first apply normal resolution to existential variables and then apply universal reduction, repeat this process again and again

3 Any QBF can be converted to skolem normal form that contains only two level of quantifiers, first existential and then universal. In this conversion, every existential variable can be replaced with a function F_x, that refers only to inner layer of universal variables. These functions are then existential quantified before those original universal variables.

This paper then describe an algorithm similar to craig interpolant, to transform the resolution proof of the QBF into the skolem functions.

MICRO'10: Register Cache System not for Latency Reduction Purpose

2011-11-22T18:03:00.002+08:00

This paper shows some astonished facts about the huge register files in wide superscalar processors:

1 The reg file is almost the same size and latency of the L1 cache

2 the reg file requires 2 or even 3 cycles to access

3 deeper pipeline for reg file increase the penalty of the speculation and also result in result shortage that leads to pipeline stall

4 deeper pipeline for reg file also leads to deep bypass network with large number of mux and long wire.

reg cache can store the most used reg file content, and leads to reduced cycle time and cycle number and power.

MICRO'10: Combating Aging with the Colt Duty Cycle Equalizer

2011-11-22T17:56:00.002+08:00

In modern CMOS process, the uneven usage of devices will make some heavily used devices approaching their failue very fast.

For example, adders are often used to add a small constant to a variable, so some devices in the higher bits of this adder are always in a constant state.

At the same time, data cache often contains more 0s than 1s.

So this paper proposes to use these devices in a more even way.

For data path components, it proposes to flip it into complementary mode instantly, in which all data are represented in 1's complementary.

For data cache, it proposes to instantly flip it into complementary mode, in which all data are stored in their 1's complementary.

For cache that suffers from uneven usage, it use LFSR to hash the index pointer, to prevent some address from heavily used, while other are not used.

For data components that suffer from uneven usage of left and right operand, it propose to swap these operand instnatly.

MICRO'10:Single-Chip Heterogeneous Computing: Does the Future Include Custom Logic, FPGAs, and GPGPUs?

2011-11-21T20:14:00.004+08:00

This paper shows that for current processors, the clock and control consume 24% power, data supply, such as data cache, consume 28% power, and instruction supply consume 42% power, the real computation only consume 6%. So over 90% power is overhead.

So it seems that combining general purpose cpu, fpga, asic and gpu in a chip is a good solution. But this paper does not give a clear conclusion yet, only bunch of figure that show trend.

MICRO'10:Voltage Smoothing: Characterizing and Mitigating Voltage Noise in Production Processors via Software-Guided Thread Scheduling

2011-11-21T19:18:00.002+08:00

This paper shows that the actions taken by the cores, such as TLB miss, branch mispredication, clock gating, will cause supply voltage swing. But actual swing is often smaller than the swing margin of the designer. So the processors are normally run in a too conservative mode, which leads to too low voltage, and therefore too slow speed.

So many papers propose to run the processors with smaller margin, and use some mechanism to recover when errors occur.

This paper proposes to measure the relationship between the voltage swing and the job run on the processor, and extrapolante this relation to wider range. It also proposes a software scheduler that help smooth the voltage swing by balancing the load on cores.

MICRO'10 : Probabilistic Distance-based Arbitration: Providing Equality of Service for Many-core CMPs

2011-11-19T16:59:00.002+08:00

In a NOC that connect multiple PE, if the router is round-robin, then a PE that is far from its communication destination can be treated very unfair in getting bandwidth, while a PE nearer can get more bandwidth.

This paper proposes use the traveling distance of a package to control the arbitrator in a router, such that fairness can be guaranteed.

MICRO'10:Fractal Coherence: Scalably Verifiable Cache Coherence

2011-11-19T16:50:00.003+08:00

This paper proposes a cache coherence protocol whose shape is fractal, which is a special case of induction.

For example, if the whole system is a tree, then for a tree of height n, this paper's approach expand one of its leaf to a small tree of height 2, then this new tree is of height n+1.

Then along the border of this newly expanded small tree, this paper tries to prove that both side can observe the other side just the SAME as the old tree.

Here, SAME doesn't just mean one to one state corresponding, instead it means one side in the new tree can have a temporal mapping of its state sequence to a single state in the old tree.

MICRO'10: Virtual Snooping: Filtering Snoops in Virtualized Multi-cores

2011-11-18T19:32:00.002+08:00

In a multi-core system running multiple Virtual machines, each VM runs on a relatively fixed set of cores, so this paper proposes a mechanism that perform snoopy based cache coherent within VM boundary.

For those rare cases that cache coherent may cross VM boundary, for example, communication between VMs and hypervisor, VM migration to new core, this mechanism provides some techniques to deal with them.

MICRO'10: Adaptive Flow Control for Robust Performance and Energy

2011-11-18T17:42:00.002+08:00

This paper proposes an NOC, whose individual router can switch between backpressured and backpressureless mode. The advantage of the former mode is its high throughput, while the latter don't use buffer in low through put application, which leads to low power overhead. The backless mode just drop contention flit or route it ramdomlly.

When two adjacent routers are in different mode, the backpressureless router will change back to backpressure mode, such that it can communicate correctly with its neighbor.

MICRO'10: ScalableBulk: Scalable Cache Coherence for Atomic Blocks in a Lazy Environment

2011-11-17T21:11:00.002+08:00

Some new architecture support execution of an atomic block of instruction(chunk), and commit their result at the end of the trunk.

When multiple processors commit at the same time, it is desirable that it is scalable.

This paper's approach:

(i) need no centralized structure,

(ii) communicate only with the relevant directories, and

(iii) allow the concurrent commit of chunks that use the same directory, as long as their addresses do not overlap.

MICRO10 : Pseudo-Circuit: Accelerating Communication for On-Chip Interconnection Networks

2011-11-04T09:55:00.001+08:00

Based on the observation that multiple flit in a package normally traverse through the same input-output pair in a router, so it is not necessary to arbitrate for every flit. So this paper propose to remember the last arbitrate result and use it for the next flit.

MICRO10: Erasing Core Boundaries for Robust and Configurable Performance

2011-11-04T09:52:00.002+08:00

Dynamically merging computation components and pipeline states to form a processor with wider data-path or a group of simple processors with narrow data-path.

This approach can also remove defective component to increase reliability.

MICRO10: Parichute: Generalized Turbocode-Based Error Correction for Near-Threshold Caches

2011-11-04T09:50:00.002+08:00

To reduce power consumption, the cache is driven by very low voltage that is near the threshold. But this may significantly increase the possibility of error. so this paper proposes to detect and correct these error with turbo code.

MICRO10:Minimal Multi-Threading: Finding and Removing Redundant Instructions in Multi-Threaded Processors

2011-11-04T09:48:00.001+08:00

Detecting instruction flow similarity between multiple thread, and only split them when they expose different computation.

Rippling: a heuristic for guiding inductive proofs

2011-10-26T07:16:00.000+08:00

It assumes that, which is actually true in most induction, the conclusion and hypothesis have almost the same structure(also called skeleton).
So rippling just convert each inferring rules of this reasoning system into a new rewriting rule, which transforms formulas with the same skeleton.
Such transformation is very similar to the rippling wave on the water surface, which is the source of the name rippling.

SOSP11: PTask: Operating System Abstractions To Manage GPUs as Compute Devices

2011-10-23T20:28:00.001+08:00

This paper provide a dataflow programming model by designing a Ptask API, which describe the dataflow between varias cmputing tasks.

These tasks can be schedule on to GPU as well as CPUs. In this way, non-neccesarry copy between devices, drivers and user codes are avoid, and the user does not need to care about the data movement explictly.

SOSP11:Scalable Consistency in Scatter

2011-10-23T20:08:00.001+08:00

There are so many papers that discuss the key-value storage, their consistency and scalability .

But I can't go into this topic because I dont have access to such environment.

MICRO10: Flexible and Efficient Instruction-Grained Run-Time Monitoring Using On-Chip Reconfigurable Fabric

2011-09-27T21:18:00.000+08:00

This paper use a FPGA to monitor the instruction stream of the main processor, which can enforce the security and array bound check requirements

MICRO10: Memory Latency Reduction via Thread Throttling

2011-09-27T21:14:00.001+08:00

This paper propose a gather computie scatter programing style that seperate the program into computing and memory thread, and schedule both of them to make sure that the number of memory thread would not over run the limited memory bandwidth.

MICRO10: The ZCache: Decoupling Ways and Associativity

2011-09-27T20:56:00.001+08:00

This paper seperate the concept of way and association.It can has small number of physical way, but large number of associations. It can access the physical way within one cycle if it hits, otherwise,it will search on the side path with multiply cycle to access more associations.

POPL02:Lazy Abstraction

2011-08-28T11:53:00.001+08:00

Today I read this paper again, and find that I have not capture its major ideas before.

Actually, It first unfold the control flow of the program to construct a tree that can reach the error position. This graph's each vertex is labeled with its own set of predicates and the reachable states formula expressed in these predicates. Its edge is labeled with the basic block of the program.

Then it backtrack and compute weakest precondition at each edge, until it find a node whose intersection of reachable state and precondition formula is empty. This will discover a new predicate by analyzing the unsat proof of this intersection .

Third, it constructs new abstract model from this pivot state to reach more errors again.

For each node reached, if it is also reached before, and the old node's label formula cover the new reached node's formula, then this node does not need to be explored any more.

CAV11:HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection

2011-08-19T17:28:00.000+08:00

What is important is the solver on strings.

CAV11:Interpolation-Based Software Verification with Wolverine

2011-08-19T17:26:00.001+08:00

This paper is not interesting, but the tool is open source, that is the point.

TACAS11:Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models

2011-08-08T12:07:00.001+08:00

This paper propose some very simple memory models for TSO and PSO, and then, I think it is the most important idea, find out whether there is some behavior on these models that can't occur in normal SC model.

FMCAD11:Effective Word-Level Interpolation for Software Verification

2011-08-07T22:47:00.003+08:00

It proposes a layered approach to generate word level interpolant for BV.

The traditional approach include two DPLL solver, one for the Boolean skeleton on the formula, the other for the conjunction of BV clauses. When a satisfying assignment is generated by the Bool solver, it is passed to the BV solver to verify it consistency.

This paper's approach inserts some layer between this two solver. These layers are over-approximation of the BV solver. They check for easier cases that can generate interpolants. For example, EUF.

FMCAD07:Lifting Propositional Interpolants to the Word-Level

2011-08-07T17:55:00.002+08:00

This paper lift the resolution tree of the SAT instance that generated from an EUF formula.

In the analysis, it not only need the resolution tree, but also the corresponding equality predicates that introduced in encoding EUF equality into CNF, and also the clause structure of this encoding.

So I can not use it to infer word level structure for a purely bit level CNF generated from complementary synthesis.

VMCAI11:SAT-Based Model Checking Without Unrolling

2011-08-07T09:33:00.000+08:00

This approach contains two nested loop,

1. in the major loop, it iteratively constructs a list of formulas F0....Fk, in which Fk means the over-approximation of the states set reachable in k steps.

2. in the minor loop, it iteratively refines the F0...Fk, such that they form an inductive path that leads to the property P to be verified.

DAC11:Re-Synthesis for Cost-Efficient Circuit-Level Timing Speculation

2011-08-07T09:32:00.002+08:00

This paper reduce the number of paths that need "Timing Speculation" by retiming to improve timing character.

And then it use ILP to share pading buffers between different paths.

MICRO03:Razor: A Low-Power Pipeline Based on Circuit-Level Timing Speculation

2011-08-07T09:32:00.001+08:00

Dynamic voltage scaling is widely used to reduce the power consumption, but it need to guarentee that all critical paths can run correctly.This may seem too conservative becasue too long path only account for a very small percent of all paths.

So this paper propose to use a shadow register to sample the critical path a little bit later than the real register, and then compare them. If the result is not the same, then a circuit is used to roll back the correct state.

One major overhead of "Timing Speculation" is the need to pad the short paths, to prevent them from making the comparator to think that a too long path has cause a timing error.

DAC11:Abstraction-Based Performance Analysis of NoCs

2011-08-07T09:31:00.000+08:00

It infers the traffic pattern for each channel in a NOC by analyzing the simulation trace generated by typical benchmarks.

This traffic pattern include the burst transition number, transition rate and bound.

And then it generate a regulator for each channel that represent this pattern and insert them into the correspoding channel, and constraint that they all hold in verification.

In this way, the traffic pattern that we interest in will be forced to hold.

This approach can also be extended to multiple channels, for example, to constrain that we dont allow five source to flood the sink at the same time, be we allow one of them to send.

Inferring Assertion for Complementary Synthesis" is accepted by ICCAD'1

2011-08-07T09:30:00.000+08:00

My paper "Inferring Assertion for Complementary Synthesis" has just been accepted by ICCAD'11.

TACAS11: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

2011-08-07T09:29:00.000+08:00

Very interesting paper that combine AC(ssociativity and commutativity) operators with Shostak approach.

Generally, there are two approaches for theory combinations, nelson-oppen and Shostak.

The former one just pass equalities between T-solvers, so it is relativly easy to combine AC with it.

But for Shostak, it need to computer canonical form, which is not possible for AC.

TACAS11: Transition Invariants and Transition Predicate Abstraction for Program Termination

2011-08-07T09:28:00.001+08:00

Very interesting.
Normal invaraints and abstraction are for states, while this paper apply them to transitions.
But I think the disjunctive well foundness is a very well known result.
I dont understand why this paper published on TACAS 11 again, these topic are well discussed before 2006.

CAV11: Verification of Certifying Computations

2011-08-07T09:27:00.001+08:00

Instead of directly verifying a program, this paper tries to verify the checker of a particular program.

This checker is actually an over-approximation of the behavior of the original program.

CAV11: Existential Quantification as Incremental SAT

2011-08-07T09:25:00.000+08:00

It use ALLSAT approach to perform existential quatification. And use increamental SAT to reduce the run time overhead.

But I think the major innovation is to use sorting network to find out the shortest prime clause. This is bettern than my approach in VMCAI05: Minimizing Counterexample with Unit Core Extraction and Incremental SAT, which reduce the size of a block clause by iteratively remove those literal not in the support set of a proof.

CAV11: Temporal property verification as a program analysis task

2011-08-07T09:24:00.000+08:00

It is a very interesting paper. Given a transition system and a temporal logc property, generate a program that search for the proof or counterexample of this property. and then use existing program analysis tools to determine that whether this program terminate with some answer.

All the methods that boost the speed, such as abstraction refinement, will be automatically performed by the program analysis tools.

TACAS'11::Optimal Base Encodings for Pseudo-Boolean Constraints

2011-03-30T16:48:00.000+08:00

This paper talk about a new method to translate the PSB problem into SAT.

Of course there are some direct solving methods, such as that of PBS solver proposed by Fadi Aloul .

But it seems that translating into SAT is also very interesting. it refer to some early papers:

1. A Translation of Pseudo-Boolean Constraints to SAT:
This paper just iterate though all coefficient, and case split on they to consider the two cases of them, and substract the correspond value from the right handside of (dis)equation.
In this way, an SAT instance is encoded.
2. Translating Pseudo-Boolean Constraints into SAT

it propose three methods
a. BDD based: similar to above method
b. adder network: it express the coefficient with a set of 2-exp, and add them together with adders.but because there are XOR gates in these adders, it is Not arc-consistent.
c. sorting network : for small coefficients n, it use n length bit vector to express it.Assume again that the sum of all coe is N, then a sorter of size N is instanced.For variables x and its coe n, x is connected to n inputs of the sorter. For right hand side x, the 0-th to x-th output of sorter is asserted to be 1.
To deal with larger coe, a set of base must be founds, such that each sorter can be used to express larger number that 1.
To minimize the size of generated SAT instance, a set of optimal base must be found, this is the motivation of this TACAS11 paper.
This TACAS11 paper propose three cost function to evaluate the total cost that need to be minimized:
a. summing the digits used to express coes: only bases with only prime numbers are need to be considered.
b. also taking into acount of the carry bits between sorters: non-prime based must be consider
c. consider the number of comparators in sorters.
With these cost function, it proposes three searching methods, they approximate the cost function and perform branch and bound searching to find a minimized cost base.

TCAD paper accepted

2010-04-12T17:14:00.001+08:00

The journal version of my iccad 2009 paper "Synthesizing Complementary Circuits Automatically." has benn accepted by IEEE Transactions on COMPUTER-AIDED DESIGN of Integrated Circuits and Systems

VMCAI'10:An Analysis of Permutations in Arrays

2010-02-04T17:49:00.003+08:00

This paper try to reason the content of data structure independent of its particular structure, for example, the sorted array has the same set of data as that of before sorting.

I also consider such problem before, but not work into it.

Basically, there are 3 types of problem
1 traditional shape analysis, such as the size and shape of data structure
2 extend above approach to deal with the relation between content and position, such as comparing two array or sortness.
3 this paper approach.

following paper even prove that such problem can't be expressed by first order logic.
Suzuki, N., Jeﬀerson, D.: Veriﬁcation decidability of Presburger array programs. J. ACM 27(1) (January 1980)

VIMCAI'10:RGSep Action Inference

2010-02-04T17:35:00.001+08:00

This paper integrate the rely-guarantee with separation logic to deal with memory problem and concurency

actually, rely is a over-approximation, while guarantee is under-approximation.

VMCAI'10: Collections, Cardinalities, and Relations

2010-02-04T17:28:00.001+08:00

This paper propose the QFBAPA-REL logic to describe the Cardinalities relation between collection like data structrue, such as list , set multi set and so on.

It can deal with problem such as "inserting an element into tree and prove that the size is increase by 1"

verification condition

2010-02-04T16:52:00.002+08:00

I finally find out what is verification condition.

For a program properly annotated with loop invariant and initial condition assertion. A logic formula is generated to express the relation between these assertion and invariants.

This logic formula is verification condition.

my ICCAD'09 paper

2010-02-03T16:57:00.002+08:00

I forget to update that, my paper had been accepted by ICCAD'09,
Synthesizing Complementary Circuits Automatically

please refer to my home page for more detail of my researching work progress.

VIMCAI'10 : Considerate Reasoning and the Composite Design Pattern

2010-02-03T16:50:00.002+08:00

the major problem of verification of imperative oo program is the complex heap structure.
One approach is the seperation logic alike approachs, including dynamic frame.

Other approaches build on the concept of object invariant, and usually sup-
port some variation of visible states semantics (with the notable exception of the
Boogie methodology [3]). In visible states semantics, object invariants should
hold at the pre- and post-states of method calls, but may be temporarily bro-
ken during method execution. Various reﬁnements have been proposed, usually
based on some notion of ownership - a way of imposing structure on the heap by
requiring that one object is encapsulated within another.

But many programming style are not in ownership style. so Considerate Reasoning is proposed.

It is based on visible states semantics; in order to support methods meant
to ﬁx invariants, it introduces the speciﬁcation construct broken. Invariants de-
clared “broken”in a method speciﬁcation are not expected to hold before calls to
the corresponding methods, but are expected to be re-established by these meth-
ods. All invariants are expected to hold at the end of a method execution.

I think such appraoch are meant to trying to find another type of ownership alike encapsule.

Some referred works

POPL'05 Separation Logic and Abstraction

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.5332&rep=rep1&type=pdf

this paper combine seperation logic with module abstaction in its reasoning rules for the first time.

FM'06 : Dynamic Frames: Support for Framing,Dependencies and Sharing Without Restrictions

This paper first state the frame approach that explictly specify the set of variables that modified by a statements.

andthen they want to invoke private viariable that is widely used in current object oriented program language, which is invisible to specification writter. so they chose to invoke specification variable for implementor, such that he can write the relation between spec var and private var.

but such approach suffer from alias pointer that can' be modeled.

so he propose an explictly approach to state the modification and preservation of sertain object.

such approach is called dynamic frame

But I think all these approaches are similar to separation logic that try to avoid specification of unmodified objects.

ICCAD'09:Interpolating Functions from Large Boolean Relations

2010-02-03T16:40:00.003+08:00

This paper use interpolation to characterize function from huge relation
http://alcom.ee.ntu.edu.tw/publications/iccad09-r2f.pdf

This solve the problem of my ICCAD'09 paper, that can't characterizeboolean function of complementary circuit efficiently.

I need to integrate this approach into my framework.

VMCAI'07:Invariant Synthesis for Combined Theories

2010-01-18T11:44:00.000+08:00

This paper infer quantifier-free invariant with pre-defined template from program with linear arithmetic and uninterpretated function.

It first translate the problem to linear programing problem by purification, that is, remove the uninterpretated functrion by defining new variable.
And then it solve the problem with linear programing.

VMCAI'10:Interpolant Strength

2009-12-29T15:52:00.002+08:00

This paper propose two approaches to generate a family of interpolants with different strength.

One approach based on labeling function, which will how to mark the internal node of a proof tree, and different function corresponding to different existing interpolant system.

And the other approach "swap" demonstrate that, by changing the order of clause the take part in the resolution, different interpolant can be obtained.

But this paper do not say how to select which strength to be used to boost model checking performance.

Come back again

2009-12-29T10:24:00.001+08:00

after 9 months of blockage by GFW, I manage to go through it with Tor.

I will now begin to update my blog again.

VMCAI09: Mostly-Functional Behavior in Java Programs

2009-03-24T13:09:00.003+08:00

it propose a type and effect system that can find out "run time constance" variables in JAVA.

I remember that I read a related paper a couple of months before, that paper discuss "stationary" field, which is similar to to this.

similar mechnism include the java standard "final" field, which is some what too restricted.

So in summary, there are three class of such mechnism:

final,too strong

stationary

quie scing

Such mechnism can prevent those variables from been initialied or writen more than one time.typical application include OO system that need to initite newlly allocated object.

Its slide describe an interesting relation between type system and effect system, the formmer one describe "what is the object",while the later one describe "how the object behave"

tacas 09 accepted papers

2008-12-20T20:30:00.003+08:00

002: The Yogi Project: Software Property Checking via Static Analysis and Testing Nori, Aditya; Thakur, Aditya; Tetali, Saideep; Rajamani, Sriram

007: Parametric Trace Slicing and Monitoring
Chen, Feng; Rosu, Grigore

015: Alpaga: A Tool for Solving Parity Games with Imperfect Information Doyen, Laurent; Berwanger, Dietmar; Chatterjee, Krishnendu; De Wulf, Martin; Henzinger, Thomas A.

016: ITPN-PerfBound: A performance bound tool for Interval Time Petri Nets Pacini, Elina Rocio; Bernardi, Simona; Gribaudo, Marco

017: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays Brummayer, Robert Daniel; Biere, Armin

022: MoonWalker: verification of .NET programs Ruys, Theo; Aan de Brugh, Niels H.M.; Nguyen, Viet Yen

028: Falsification of LTL Safety Properties in Hybrid Systems
Plaku, Erion; Kavraki, Lydia; Vardi, Moshe

032: Ground Interpolation for the Theory of Equality Krstic, Sava; Fuchs, Alexander; Goel, Amit; Grundy, Jim; Tinelli, Cesare

033: All-Termination(T)
Turon, Aaron; Manolios, Panagiotis

043: Test input generation for programs with pointers
Vanoverberghe, Dries; Tillmann, Nikolai; Piessens, Frank

044: Compositional Predicate Abstraction from Game Semantics
Ghica, Dan; Bakewell, Adam

048: Memoised Garbage Collection for Software Model Checking
Nguyen, Viet Yen; Ruys, Theo

051: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications Segall, Itai; Kugler, Hillel

065: Computing Optimized Representations for Non-Convex Polyhedra by Detection and Removal of Redundant Linear Constraints Disch, Stefan; Scholl, Christoph; Pigorsch, Florian; Kupferschmid, Stefan

073: Static Analysis Techniques for Parameterised Boolean Equation Systems Willemse, Tim; Orzan, Simona; Wesselink, Wieger

082: Semantic Reduction of Thread Interleavings for Concurrent Programs
Gupta, Aarti; Kahlon, Vineet; Sankaranarayanan, Sriram

084: Computing Weakest Strategies for Safety Games of Imperfect Information Kuijper, Wouter; Pol, Jaco

085: Buechi Complementation and Size-Change Termination
Fogarty, Seth; Vardi, Moshe

086: Path Feasibility Analysis for String-Manipulating Programs
Bjorner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei

088: TaPAS : The Talence Presburger Arithmetic Suite
Leroux, Jerome; Point, Gerald

91: Satisfiability Procedures for Combination of Theories Sharing
Integer Offsets
Ringeissen, Christophe; Nicolini, Enrica; Rusinowitch, Michael

094: Hierarchical Adaptive State Space Caching based on Level Sampling
Wijs, Anton; Mateescu, Radu

095: Transition-based Directed Model Checking Kupferschmid, Sebastian; Wehrle, Martin; Podelski, Andreas

101: Context-bounded analysis for concurrent programs with dynamic creation of threads Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz

113: Romeo : A Parametric Model-Checker for Petri Nets with Stopwatches Traonouez, Louis-Marie; Lime, Didier; Roux, Olivier (H.); Seidner, Charlotte

117: Verifying Reference Counting Implementations Emmi, Michael; Kohler, Eddie; Jhala, Ranjit; Majumdar, Rupak

118: RBAC-PAT: A Policy Analysis Tool for Role Based Access Control Yang, Ping; Stoller, Scott; Zhang, Yingbin; Solomon, Ayla; Luo, Ruiqi; Gofman, Mikhail

120: Hierachical Set Decision Diagrams and Regular Models Thierry-Mieg, Yann; Poitrenaud, Denis; Hamez, Alexandre; Kordon, Fabrice

137: Inferring Synchronization under Limited Observability Yorsh, Greta; Yahav, Eran; Vechev, Martin

141: Learning Minimal Separating DFA's for Compositional Verification Chen, Yu-Fang; larke, Edmund; Farzan, Azadeh; Tsay, Yih-Kuen; Wang, Bow-Yaw

144: An Efficient Invariant Generator
Majumdar, Rupak; Gupta, Ashutosh; Rybalchenko, Andrey

146: Specification Mining With Few False Positives Le Goues, Claire; Weimer, Westley

149: Symbolic String Verification: Combining String Analysis and Size Analysis Yu, Fang; Ibarra, Oscar H.; Bultan, Tevfik

160: The Complexity of Predicting Atomicity Violations Farzan, Azadeh; Parthasarathy, Madhusudan

169: Iterating Octagons
IOSIF, Radu; Bozga, Marius; Girlea, Codruta

centos 5.2 dont include g++ by default installation

2008-11-06T19:51:00.001+08:00

While I compile zchaff sat solver under centos 5.2, it complain that dont find g++. it is actually in gcc-c++-4.1.2-42.el5.x86_64.rpm. just install it and everything ok

exploring similarity between sub constructor

2008-11-06T09:03:00.002+08:00

there are some degree of similarity between sub constructors, and some operation only care such similarity, and dont care the difference.

for example, in a verilog parser, there is a data onstructor like this,
and blocking_assignment =
T_blocking_assignment_direct of lvalue*expression
| T_blocking_assignment_delay of lvalue*expression*delay_control
| T_blocking_assignment_event of lvalue*expression*event_control
and non_blocking_assignment =
T_non_blocking_assignment_direct of lvalue*expression
| T_non_blocking_assignment_delay of lvalue*expression*delay_control
| T_non_blocking_assignment_event of lvalue*expression*event_control

and in one operation regs, I only need to get the left value list, so I only care lvalue part,
In another operation deps, I only need to get the variables appear on right hand side, so I only need the expression part.

So can we just specify lvalue and expression without mention the exact constructor name and other data?

disabling of mihuo protocol

2008-11-05T23:41:00.001+08:00

I use amule to download resource of verycd, but it just refuse to start, and complain about low ID,

I notice that there are mihuo protocol setting, so I just disable it , and everything OK

formal method to warn us about the effect of updated environment

2008-11-04T09:51:00.001+08:00

When we or other people other then we, modify some code incrementally, then it will afect the proper treatment of the other code, so can we develop a metnod to warn us about what to do when it is need?

bridge the gap of my mind and the state of the art library

2008-11-04T09:47:00.002+08:00

When we try to use a library, we has some idea about its functionality and structrue in our mind, which can be seen as an abstraction of the library.

So if there exist a method to connect this our mind with the actual lib?

ICSE 08:ReBA: Refactoring-aware Binary Adaptation of Evolving Libraries

2008-10-29T16:06:00.001+08:00

This paper propose to synthesis a compatible layer on new version library,to make the old code run correctly.

This idea is also in my mind for a long time.

Incremental State-Space Exploration for Programs with Dynamically Allocated Data

2008-10-29T16:03:00.001+08:00

OH,another idea that pop up in my mind but have not followed.

This paper deal with increamental state space exploration for Programs with Dynamically Allocated Data