bluuebunny/crossref_metadata_2025 huggingface dataset:
ReQoS
Authors: Tang Lingjia , Mars Jason , Wang Wei , Dey Tanima , Soffa Mary Lou
Published: July 2013

As multicore processors with expanding core counts continue to dominate the server market, the overall utilization of the class of datacenters known as
warehouse scale computers
(WSCs) depends heavily on colocation of multiple workloads on each server to take advantage of the computational power provided by modern processors. However, many of the applications running in WSCs, such as websearch, are user-facing and have quality of service (QoS) requirements. When multiple applications are co-located on a multicore machine, contention for shared memory resources threatens application QoS as severe cross-core performance interference may occur. WSC operators are left with two options: either disregard QoS to maximize WSC utilization, or disallow the co-location of high-priority user-facing applications with other applications, resulting in low machine utilization and millions of dollars wasted.

This paper presents ReQoS, a static/dynamic compilation approach that enables low-priority applications to adaptively manipulate their own contentiousness to ensure the QoS of high-priority co-runners. ReQoS is composed of a profile guided compilation technique that identifies and inserts markers in contentious code regions in low-priority applications, and a lightweight runtime that monitors the QoS of high-priority applications and reactively reduces the pressure low-priority applications generate to the memory subsystem when cross-core interference is detected. In this work, we show that ReQoS can accurately diagnose contention and significantly reduce performance interference to ensure application QoS. Applying ReQoS to SPEC2006 and SmashBench workloads on real multicore machines, we are able to improve machine utilization by more than 70% in many cases, and more than 50% on average, while enforcing a 90% QoS threshold. We are also able to improve the energy efficiency of modern multicore machines by 47% on average over a policy of disallowing co-locations.
Production-run software failure diagnosis via hardware performance counters
Authors: Arulraj Joy , Chang Po-Chun , Jin Guoliang , Lu Shan
Published: July 2013

Sequential and concurrency bugs are widespread in deployed software. They cause severe failures and huge financial loss during production runs. Tools that diagnose production-run failures with low overhead are needed. The state-of-the-art diagnosis techniques use software instrumentation to sample program properties at run time and use off-line statistical analysis to identify properties most correlated with failures. Although promising, these techniques suffer from high run-time overhead, which is sometimes over 100%, for concurrency-bug failure diagnosis and hence are not suitable for production-run usage.

We present PBI, a system that uses existing hardware performance counters to diagnose production-run failures caused by sequential and concurrency bugs with low overhead. PBI is designed based on several key observations. First, a few widely supported performance counter events can reflect a wide variety of common software bugs and can be monitored by hardware with almost no overhead. Second, the counter overflow interrupt supported by existing hardware and operating systems provides a natural and effective mechanism to conduct event sampling at user level. Third, the noise and non-determinism in interrupt delivery complements well with statistical processing.

We evaluate PBI using 13 real-world concurrency and sequential bugs from representative open-source server, client, and utility programs, and 10 bugs from a widely used software-testing benchmark. Quantitatively, PBI can effectively diagnose failures caused by these bugs with a small overhead that is never higher than 10%. Qualitatively, PBI does not require any change to software and presents a novel use of existing hardware performance counters.
Transparent mutable replay for multicore debugging and patch validation
Authors: Viennot Nicolas , Nair Siddharth , Nieh Jason
Published: July 2013

We present Dora, a mutable record-replay system which allows a recorded execution of an application to be replayed with a modified version of the application. This feature, not available in previous record-replay systems, enables powerful new functionality. In particular, Dora can help reproduce, diagnose, and fix software bugs by replaying a version of a recorded application that is recompiled with debugging information, reconfigured to produce verbose log output, modified to include additional print statements, or patched to fix a bug.

Dora uses lightweight operating system mechanisms to record an application execution by capturing nondeterministic events to a log without imposing unnecessary timing and ordering constraints. It replays the log using a modified version of the application even in the presence of added, deleted, or modified operations that do not match events in the log. Dora searches for a replay that minimizes differences between the log and the replayed execution of the modified program. If there are no modifications, Dora provides deterministic replay of the unmodified program.

We have implemented a Linux prototype which provides transparent mutable replay without recompiling or relinking applications. We show that Dora is useful for reproducing, diagnosing, and fixing software bugs in real-world applications, including Apache and MySQL. Our results show that Dora (1) captures bugs and replays them with applications modified or reconfigured to produce additional debugging output for root cause diagnosis, (2) captures exploits and replays them with patched applications to validate that the patches successfully eliminate vulnerabilities, (3) records production workloads and replays them with patched applications to validate patches with realistic workloads, and (4) maintains low recording overhead on commodity multicore hardware, making it suitable for production systems.
Computational sprinting on a hardware/software testbed
Authors: Raghavan Arun , Emurian Laurel , Shao Lei , Papaefthymiou Marios , Pipe Kevin P. , Wenisch Thomas F. , Martin Milo M.K.
Published: July 2013

CMOS scaling trends have led to an inflection point where thermal constraints (especially in mobile devices that employ only passive cooling) preclude sustained operation of all transistors on a chip --- a phenomenon called "dark silicon." Recent research proposed computational sprinting --- exceeding sustainable thermal limits for short intervals --- to improve responsiveness in light of the bursty computation demands of many media-rich interactive mobile applications. Computational sprinting improves responsiveness by activating reserve cores (parallel sprinting) and/or boosting frequency/voltage (frequency sprinting) to power levels that far exceed the system's sustainable cooling capabilities, relying on thermal capacitance to buffer heat.

Prior work analyzed the feasibility of sprinting through modeling and simulation. In this work, we investigate sprinting using a hardware/software testbed. First, we study unabridged sprints, wherein the computation completes before temperature becomes critical, demonstrating a 6.3x responsiveness gain, and a 6% energy efficiency improvement by racing to idle. We then analyze truncated sprints, wherein our software runtime system must intervene to prevent overheating by throttling parallelism and frequency before the computation is complete. To avoid oversubscription penalties (context switching inefficiencies after a truncated parallel sprint), we develop a sprint-aware task-based parallel runtime. We find that maximal-intensity sprinting is not always best, introduce the concept of sprint pacing, and evaluate an adaptive policy for selecting sprint intensity. We report initial results using a phase change heat sink to extend maximum sprint duration. Finally, we demonstrate that a sprint-and-rest operating regime can actually outperform thermally-limited sustained execution.
Iago attacks
Authors: Checkoway Stephen , Shacham Hovav
Published: July 2013

In recent years, researchers have proposed systems for running trusted code on an untrusted operating system. Protection mechanisms deployed by such systems keep a malicious kernel from directly manipulating a trusted application's state. Under such systems, the application and kernel are, conceptually, peers, and the system call API defines an RPC interface between them.

We introduce
Iago attacks
, attacks that a malicious kernel can mount in this model. We show how a carefully chosen sequence of integer return values to Linux system calls can lead a supposedly protected process to act against its interests, and even to undertake arbitrary computation at the malicious kernel's behest.

Iago attacks are evidence that protecting applications from malicious kernels is more difficult than previously realized.
Verifying security invariants in ExpressOS
Authors: Mai Haohui , Pek Edgar , Xue Hui , King Samuel Talmadge , Madhusudan Parthasarathy
Published: July 2013

Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our use of formal methods for proving key security invariants about our implementation. In our use of formal methods, we focus solely on proving that our OS implements our security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of our system.

We built ExpressOS, analyzed its security, and tested its performance. Our evaluation shows that the performance of ExpressOS is comparable to an Android-based system. In one test, we ran the same web browser on ExpressOS and on an Android-based system, and found that ExpressOS adds 16% overhead on average to the page load latency time for nine popular web sites.
Verifying systems rules using rule-directed symbolic execution
Authors: Cui Heming , Hu Gang , Wu Jingyue , Yang Junfeng
Published: July 2013

Systems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is symbolic execution, a technique that verifies program paths over all inputs up to a bounded size. However, when applied to verify rules, existing symbolic execution systems often blindly explore many redundant program paths while missing relevant ones that may contain bugs.

Our key insight is that only a small portion of paths are relevant to rules, and the rest (majority) of paths are irrelevant and do not need to be verified. Based on this insight, we create WOODPECKER, a new symbolic execution system for effectively checking rules on systems programs. It provides a set of builtin checkers for common rules, and an interface for users to easily check new rules. It directs symbolic execution toward the program paths relevant to a checked rule, and soundly prunes redundant paths, exponentially speeding up symbolic execution. It is designed to be heuristic-agnostic, enabling users to leverage existing powerful search heuristics.

Evaluation on 136 systems programs totaling 545K lines of code, including some of the most widely used programs, shows that, with a time limit of typically just one hour for each verification run, WOODPECKER effectively verifies 28.7% of the program and rule combinations over bounded input, whereas an existing symbolic execution system KLEE verifies only 8.5%. For the remaining combinations, WOODPECKER verifies 4.6 times as many relevant paths as KLEE. With a longer time limit, WOODPECKER verifies much more paths than KLEE,
e.g.,
17 times as many with a fourhour limit. WOODPECKER detects 113 rule violations, including 10 serious data loss errors with 2 most serious ones already confirmed by the corresponding developers.
TSO_ATOMICITY
Authors: Wang Cheng , Wu Youfeng
Published: July 2013

Program optimizations based on data dependences may not preserve the memory consistency in the programs. Previous works leverage a hardware ATOMICITY primitive to restrict the thread interleaving for preserving
sequential consistency
in region optimizations. However, ATOMICITY primitive is over restrictive on the thread interleaving for optimizing real-world applications developed with the popular
Total-Store-Ordering
(TSO) memory consistency, which is weaker than sequential consistency. In this paper, we present a novel hardware TSO_ATOMICITY primitive, which has less restriction on the thread interleaving than ATOMICITY primitive to permit more efficient program execution than ATOMICITY primitive, but can still preserve TSO memory consistency in all region optimizations. Furthermore, TSO_ATOMICITY primitive requires similar architecture support as ATOMICITY primitive and can be implemented with only slight change to the existing ATOMICITY primitive implementation. Our experimental results show that in a start-of-art dynamic binary optimization system on a large set of workloads, ATOMICITY primitive can only improve the performance by 4% on average. TSO_ATOMICITY primitive can reduce the overhead associated with ATOMICITY primitive and improve the performance by 12% on average.
Volition
Authors: Qian Xuehai , Torrellas Josep , Sahelices Benjamin , Qian Depei
Published: July 2013

Sequential Consistency (SC) is the most intuitive memory model, and SC Violations (SCVs) produce unintuitive, typically incorrect executions. Most prior SCV detection schemes have used data races as proxies for SCVs, which is highly imprecise. Other schemes that have targeted data-race cycles are either too conservative or are designed only for two-processor cycles and snoopy-based systems.

This paper presents Volition, the first hardware scheme that detects SCVs in a relaxed-consistency machine precisely, in a scalable manner, and for an arbitrary number of processors in the cycle. Volition leverages cache coherence protocol transactions to dynamically detect cycles in memory-access orders across threads. When a cycle is about to occur, an exception is triggered. Volition can be used in both directory- and snoopy-based coherence protocols. Our simulations of Volition in a 64-processor multicore with directory-based coherence running SPLASH-2 and Parsec programs shows that Volition induces negligible traffic and execution overhead. In addition, it can detect SCVs with several processors. Volition is suitable for on-the-fly use.
Hardware support for fine-grained event-driven computation in Anton 2
Authors: Grossman J. P. , Kuskin Jeffrey S. , Bank Joseph A. , Theobald Michael , Dror Ron O. , Ierardi Douglas J. , Larson Richard H. , Schafer U. Ben , Towles Brian , Young Cliff , Shaw David E.
Published: July 2013

Exploiting parallelism to accelerate a computation typically involves dividing it into many small tasks that can be assigned to different processing elements. An efficient execution schedule for these tasks can be difficult or impossible to determine in advance, however, if there is uncertainty as to when each task's input data will be available. Ideally, each task would run in direct response to the arrival of its input data, thus allowing the computation to proceed in a fine-grained event-driven manner. Realizing this ideal is difficult in practice, and typically requires sacrificing flexibility for performance.

In Anton 2, a massively parallel special-purpose supercomputer for molecular dynamics simulations, we addressed this challenge by including a hardware block, called the dispatch unit, that provides flexible and efficient support for fine-grained event-driven computation. Its novel features include a many-to-many mapping from input data to a set of synchronization counters, and the ability to prioritize tasks based on their type. To solve the additional problem of using a fixed set of synchronization counters to track input data for a potentially large number of tasks, we created a software library that allows programmers to treat Anton 2 as an idealized machine with infinitely many synchronization counters. The dispatch unit, together with this library, made it possible to simplify our molecular dynamics software by expressing it as a collection of independent tasks, and the resulting fine-grained execution schedule improved overall performance by up to 16% relative to a coarse-grained schedule for precisely the same computation.
The role of C in the dark ages of multi-core
Authors: Beemster Marcel
Published: July 2013

Contrary to predictions of its demise, C remains a dominant programming language, especially in embedded systems. Speed and transparency dictate that it will be so for the next decade, despite its supposed unsuitability for programming parallel architectures. A flexible compiler development system is a unique vehicle to bend the C language and its implementation to the developers' will. Using hard-won experience in applying extended versions of C to diverse parallel architectures, C's potential in the dark ages of multi-core programming is examined.
Practical speculative parallelization of variable-length decompression algorithms
Authors: Jang Hakbeom , Kim Channoh , Lee Jae W.
Published: July 2013

Variable-length coding is widely used for efficient data compression. Typically, the compressor splits the original data into blocks and compresses each block with variable-length codes, hence producing variable-length compressed blocks. Although the compressor can easily exploit ample block-level parallelism, it is much more difficult to extract such coarse-grain parallelism from the decompressor because a block boundary cannot be located until decompression of the previous block is completed. This paper presents novel algorithms to efficiently predict block boundaries and a runtime system that enables efficient block-level parallel decompression, called
SDM
. The SDM execution model features speculative pipelining with three stages: Scanner, Decompressor, and Merger. The scanner stage employs a high-confidence prediction algorithm that finds compressed block boundaries without fully decompressing individual blocks. This information is communicated to the parallel decompressor stage in which multiple blocks are decompressed in parallel. The decompressed blocks are merged in order by the merger stage to produce the final output. The SDM runtime is specialized to execute this pipeline correctly and efficiently on resource-constrained embedded platforms. With SDM we effectively parallelize three production-grade variable-length
decompression
algorithms?zlib, bzip2, and H.264?with maximum speedups of 2.50× and 8.53× (and geometric mean speedups of 1.96× and 4.04×) on 4-core and 36-core embedded platforms, respectively.
Boosting efficiency of fault detection and recovery throughapplication-specific comparison and checkpointing
Authors: Chen Hao , Yang Chengmo
Published: July 2013

While the unending technology scaling has brought reliability to the forefront of concerns of semiconductor industry, fault tolerance techniques are still rarely incorporated into existing designs due to their high overhead. One fault tolerance scheme that receives a lot of research attention is duplication and checkpointing. However, most of the techniques in the category employ a blind strategy to compare instruction results, therefore not only generating large overhead in buffering and verifying these values, but also inducing unnecessary rollbacks to recover faults that will never influence subsequent execution. To tackle these issues, we introduce in this paper an approach that identifies the minimum set of instruction results for fault detection and checkpointing. For a given application, the proposed technique first identifies the control and data flow information of each execution hotspot, and then selects only the instruction results that either influence the final program results or are needed during re-execution as the comparison set. Our experimental studies demonstrate that the proposed hotspot-targeting technique is able to reduce nearly 88% of the comparison overhead and mask over 38% of the total injected faults of all the injected faults while at the same time delivering full fault coverage.
Compiler directed write-mode selection for high performance low power volatile PCM
Authors: Li Qingan , Jiang Lei , Zhang Youtao , He Yanxiang , Xue Chun Jason
Published: July 2013

Micro-Controller Units (MCUs) are widely adopted ubiquitous computing devices. Due to tight cost and energy constraints, MCUs often integrate very limited internal RAM memory on top of Flash storage, which exposes Flash to heavy write traffic and results in short system lifetime. Architecting emerging Phase Change Memory (PCM) is a promising approach for MCUs due to its fast read speed and long write endurance.

However, PCM, especially multi-level cell (MLC) PCM, has long write latency and requires large write energy, which diminishes the benefits of its replacement of traditional Flash. By studying MLC PCM write operations, we observe that writing MLC PCM can take advantages of two write modes --- fast write leaves cells in volatile state, and slow write leaves cells in non-volatile state. In this paper, we propose a compiler directed dual-write (CDDW) scheme that selects the best write mode for each write operation to maximize the overall performance and energy efficiency. Our experimental results show that CDDW reduces dynamic energy by 32.4%(33.8%) and improves performance by 6.3%(35.9%) compared with an all fast(slow) write approach.
Program performance spectrum
Authors: Chattopadhyay Sudipta , Chong Lee Kee , Roychoudhury Abhik
Published: July 2013

Real-time and embedded applications often need to satisfy several non-functional properties such as timing. Consequently, performance validation is a crucial stage before the deployment of real-time and embedded software. Cache memories are often used to bridge the performance gap between a processor and memory subsystems. As a result, the analysis of caches plays a key role in the performance validation of real-time, embedded software. In this paper, we propose a novel approach to compute the cache performance signature of an entire program. Our technique is based on exploring the input domain through different path programs. Two paths belong to the same path program if they follow the same set of control flow edges but may vary in the iterations of loops encountered. Our experiments with several subject programs show that the different paths grouped into a path program have very similar and often exactly same cache performance.

Our path program exploration can be viewed as partitioning the input domain of the program. Each partition is associated with its cache performance and a symbolic formula capturing the set of program inputs which constitutes the partition. We show that such a partitioning technique has wide spread usages in performance prediction, testing, debugging and design space exploration.
Portable mapping of openMP to multicore embedded systems using MCA APIs
Authors: Wang Cheng , Chandrasekaran Sunita , Sun Peng , Chapman Barbara , Holt Jim
Published: July 2013

Multicore embedded systems are being widely used in telecommunication systems, robotics, medical applications and more.While they offer a high-performance with low-power solution, programming in an efficient way is still a challenge. In order to exploit the capabilities that the hardware offers, software developers are expected to handle many of the low-level details of programming including utilizing DMA, ensuring cache coherency, and inserting synchronization primitives explicitly. The state-of-the-art involves solutions where the software toolchain is too vendor-specific thus tying the software to a particular hardware leaving no room-for portability.

In this paper we present a runtime system to explore mapping a high-level programming model, OpenMP, on to multicore embedded systems. A key feature of our scheme is that unlike the existing approaches that largely rely on POSIX threads, our approach leverages the Multicore Association (MCA) APIs as an OpenMP translation layer. The MCA APIs is a set of low-level APIs handling resource management, inter-process communications and task scheduling for multicore embedded systems. By deploying the MCA APIs, our runtime is able to effectively capture the characteristics of multicore embedded systems compared with the POSIX threads. Furthermore, the MCA layer enables our runtime implementation to be portable across various architectures. Thus programmers only need to maintain a single OpenMP code base which is compatible by various compilers, while on the other hand, the code is portable across different possible types of platforms. We have evaluated our runtime system using several embedded benchmarks. The experiments demonstrate promising and competitive performance compared to the native approach for the platform.
A two-step optimization technique for functions placement, partitioning, and priority assignment in distributed systems
Authors: Mehiaoui Asma , Wozniak Ernest , Tucci-Piergiovanni Sara , Mraidha Chokri , Di Natale Marco , Zeng Haibo , Babau Jean-Philippe , Lemarchand Laurent , Gerard Sébastien
Published: July 2013

Modern development methodologies from the industry and the academia for complex real-time systems define a stage in which application functions are deployed onto an execution platform. The deployment consists of the placement of functions on a distributed network of nodes, the partitioning of functions in tasks and the scheduling of tasks and messages. None of the existing optimization techniques deal with the three stages of the deployment problem at the same time. In this paper, we present a staged approach towards the efficient deployment of real-time functions based on genetic algorithms and mixed integer linear programming techniques. Application to case studies shows the applicability of the method to industry-size systems and the quality of the obtained solutions when compared to the true optimum for small size examples.
Look up!
Authors: Larus James R.
Published: July 2013

The "Cloud" is a wonderfully expansive phrase used to denote computation and data storage centralized in a large datacenter and elastically accessed across a network. The concept is not new; web sites and business servers have run in datacenters for a long time. These, however, were specialized applications, outside of the mainstream of desktop programs. The past few years has seen enormous change as the mainstream shifts from a single computer to mobile devices and clusters of computers. Three factors are driving this change. 1) Mobile computing, where apps run on a size- and power-constrained device and would be far less interesting without backend systems to augment computation and storage capacity. 2) Big data, which uses clusters of computers to extract valuable information from vast amounts of unstructured data. 3) Inexpensive, elastic computing, pioneered by Amazon Web Services, which enables everyone to rapidly obtain and use many servers.

As a researcher from the language and compiler community, I firmly believe this sea change is at heart a programming problem. Cloud computing is far different from the environment in which most of today's languages and tools were developed, and few programmers have mastered its complexity. New challenges include pervasive parallelism, partial failure, high and variable communication latency, and replication for reliability and throughput.
Rely-guarantee references for refinement types over aliased mutable data
Authors: Gordon Colin S. , Ernst Michael D. , Grossman Dan
Published: July 2013

Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions in the presence of aliasing and side effects, unifying ideas from reference immutability type systems and rely-guarantee program logics. Our approach, rely-guarantee references, treats multiple references to shared objects similarly to multiple threads in rely-guarantee program logics. We propose statically associating rely and guarantee conditions with individual references to shared objects. Multiple aliases to a given object may coexist only if the guarantee condition of each alias implies the rely condition for all other aliases. We demonstrate that existing reference immutability type systems are special cases of rely-guarantee references.

In addition to allowing precise control over state modification, rely-guarantee references allow types to depend on mutable data while still permitting flexible aliasing. Dependent types whose denotation is stable over the actions of the rely and guarantee conditions for a reference and its data will not be invalidated by any action through any alias. We demonstrate this with refinement (subset) types that may depend on mutable data. As a special case, we derive the first reference immutability type system with dependent types over immutable data.

We show soundness for our approach and describe experience using rely-guarantee references in a dependently-typed monadic DSL in Coq.
Terra
Authors: DeVito Zachary , Hegarty James , Aiken Alex , Hanrahan Pat , Vitek Jan
Published: July 2013

High-performance computing applications, such as auto-tuners and domain-specific languages, rely on generative programming techniques to achieve high performance and portability. However, these systems are often implemented in multiple disparate languages and perform code generation in a separate process from program execution, making certain optimizations difficult to engineer. We leverage a popular scripting language, Lua, to stage the execution of a novel low-level language, Terra. Users can implement optimizations in the high-level language, and use built-in constructs to generate and execute high-performance Terra code. To simplify meta-programming, Lua and Terra share the same lexical environment, but, to ensure performance, Terra code can execute independently of Lua's runtime. We evaluate our design by reimplementing existing multi-language systems entirely in Terra. Our Terra-based auto-tuner for BLAS routines performs within 20% of ATLAS, and our DSL for stencil computations runs 2.3x faster than hand-written C.
CLAP
Authors: Huang Jeff , Zhang Charles , Dolby Julian
Published: July 2013

We present CLAP, a new technique to reproduce concurrency bugs. CLAP has two key steps. First, it logs thread local execution paths at runtime. Second, offline, it computes memory dependencies that accord with the logged execution and are able to reproduce the observed bug. The second step works by combining constraints from the thread paths and constraints based on a memory model, and computing an execution with a constraint solver.

CLAP has four major advantages. First, logging purely local execution of each thread is substantially cheaper than logging memory interactions, which enables CLAP to be efficient compared to previous approaches. Second, our logging does not require any synchronization and hence with no added memory barriers or fences; this minimizes perturbation and missed bugs due to extra synchronizations foreclosing certain racy behaviors. Third, since it uses no synchronization, we extend CLAP to work on a range of relaxed memory models, such as TSO and PSO, in addition to sequential consistency. Fourth, CLAP can compute a much simpler execution than the original one, that reveals the bug with minimal thread context switches. To mitigate the scalability issues, we also present an approach to parallelize constraint solving, which theoretically scales our technique to programs with arbitrary execution length.

Experimental results on a variety of multithreaded benchmarks and real world concurrent applications validate these advantages by showing that our technique is effective in reproducing concurrency bugs even under relaxed memory models; furthermore, it is significantly more efficient than a state-of-the-art technique that records shared memory dependencies, reducing execution time overhead by 45% and log size by 88% on average.
It's alive! continuous feedback in UI programming
Authors: Burckhardt Sebastian , Fahndrich Manuel , de Halleux Peli , McDirmid Sean , Moskal Michal , Tillmann Nikolai , Kato Jun
Published: July 2013

Live programming allows programmers to edit the code of a running program and immediately see the effect of the code changes. This tightening of the traditional edit-compile-run cycle reduces the cognitive gap between program code and execution, improving the learning experience of beginning programmers while boosting the productivity of seasoned ones. Unfortunately, live programming is difficult to realize in practice as imperative languages lack well-defined abstraction boundaries that make live programming responsive or its feedback comprehensible.

This paper enables live programming for user interface programming by cleanly separating the rendering and non-rendering aspects of a UI program, allowing the display to be refreshed on a code change without restarting the program. A type and effect system formalizes this separation and provides an evaluation model that incorporates the code update step. By putting live programming on a more formal footing, we hope to enable critical and technical discussion of live programming systems.
Static analysis for probabilistic programs
Authors: Sankaranarayanan Sriram , Chakarov Aleksandar , Gulwani Sumit
Published: July 2013

We propose an approach for the static analysis of probabilistic programs that sense, manipulate, and control based on uncertain data. Examples include programs used in risk analysis, medical decision making and cyber-physical systems. Correctness properties of such programs take the form of queries that seek the probabilities of assertions over program variables. We present a static analysis approach that provides guaranteed interval bounds on the values (assertion probabilities) of such queries. First, we observe that for probabilistic programs, it is possible to conclude facts about the behavior of the entire program by choosing a finite, adequate set of its paths. We provide strategies for choosing such a set of paths and verifying its adequacy. The queries are evaluated over each path by a combination of symbolic execution and probabilistic volume-bound computations. Each path yields interval bounds that can be summed up with a "coverage" bound to yield an interval that encloses the probability of assertion for the program as a whole. We demonstrate promising results on a suite of benchmarks from many different sources including robotic manipulators and medical decision making programs.
Reasoning about nondeterminism in programs
Authors: Cook Byron , Koskinen Eric
Published: July 2013

Branching-time temporal logics (e.g. CTL, CTL*, modal mu-calculus) allow us to ask sophisticated questions about the nondeterminism that appears in systems. Applications of this type of reasoning include planning, games, security analysis, disproving, precondition synthesis, environment synthesis, etc. Unfortunately, existing automatic branching-time verification tools have limitations that have traditionally restricted their applicability (e.g. push-down systems only, universal path quantifiers only, etc).

In this paper we introduce an automation strategy that lifts many of these previous restrictions. Our method works reliably for properties with non-trivial mixtures of universal and existential modal operators. Furthermore, our approach is designed to support (possibly infinite-state) programs.

The basis of our approach is the observation that existential reasoning can be reduced to universal reasoning if the system's state-space is appropriately restricted. This restriction on the state-space must meet a constraint derived from recent work on proving non-termination. The observation leads to a new route for implementation based on existing tools. To demonstrate the practical viability of our approach, we report on the results applying our preliminary implementation to a set of benchmarks drawn from the Windows operating system, the PostgreSQL database server, SoftUpdates patching system, as well as other hand-crafted examples.
Darkness at the End of the Tunnel: Poststenotic Kidney Injury
Authors: Eirin Alfonso , Lerman Lilach O.
Published: July 2013

Renal artery stenosis remains an important contributor to renal failure in the elderly population, but uncertainty continues to surround the mechanisms underlying progressive renal dysfunction. Here, we present the current understanding of the pathogenic mechanisms responsible for renal injury in these patients, with emphasis on those involved in disease progression.
Role of β-Adrenergic Receptors and Nitric Oxide Signaling in Exercise-Mediated Cardioprotection
Authors: Calvert John W. , Lefer David J.
Published: July 2013

Exercise promotes cardioprotection in both humans and animals not only by reducing risk factors associated with cardiovascular disease but by reducing myocardial infarction and improving survival following ischemia. This article will define the role that nitric oxide and β-adrenergic receptors play in mediating the cardioprotective effects of exercise in the setting of ischemia-reperfusion injury.
Activating Autoantibodies and Cardiovascular Disease
Authors: Luft Friedrich C.
Published: July 2013

Stimulating antibodies against G-protein-coupled receptors, including the β1- and β2-adrenergic receptors, the α1-adrenergic receptor, and the angiotensin II AT1 receptor, have been described, as well as activating antibodies directed at the platelet-derived growth factor receptor tyrosine kinase. Their existence and actions appear to be established. Lacking are mechanistic studies of receptor activation and translational studies to document receptor-stimulating antibodies as worthwhile therapeutic targets.
Approximate Analytical Solutions of Fractional Perturbed Diffusion Equation by Reduced Differential Transform Method and the Homotopy Perturbation Method
Authors: Cui Zhoujin , Mao Zisen , Yang Sujuan , Yu Pinneng
Published: July 2013

The approximate analytical solutions of differential equations with fractional time derivative are obtained with the help of a general framework of the reduced differential transform method (RDTM) and the homotopy perturbation method (HPM). RDTM technique does not require any discretization, linearization, or small perturbations and therefore it reduces significantly the numerical computation. Comparing the methodology (RDTM) with some known technique (HPM) shows that the present approach is effective and powerful. The numerical calculations are carried out when the initial conditions in the form of periodic functions and the results are depicted through graphs. The two different cases have studied and proved that the method is extremely effective due to its simplistic approach and performance.
A Steganographic Method Based on Pixel-Value Differencing and the Perfect Square Number
Authors: Tseng Hsien-Wen , Leng Hui-Shih
Published: July 2013

The pixel-value differencing (PVD) scheme uses the difference value between two consecutive pixels in a block to determine how many secret bits should be embedded. There are two types of the quantization range table in Wu and Tasi's method. The first was based on selecting the range widths of [8, 8, 16, 32, 64, 128], to provide large capacity. The second was based on selecting the range widths of [2, 2, 4, 4, 4, 8, 8, 16, 16, 32, 32, 64, 64], to provide high imperceptibility. Most of the related studies focus on increasing the capacity using LSB and the readjustment process, so their approach is too conformable to the LSB approach. There are very few studies focusing on the range table design. Besides, it is intuitive to design it by using the width of the power of two. This work designs a new quantization range table based on the perfect square number to decide the payload by the difference value between the consecutive pixels. Our research provides a new viewpoint that if we choose the proper width for each range and use the proposed method, we can obtain better image quantity and higher capacity. In addition, we offer a theoretical analysis to show our method is well defined. The experiment results also show the proposed scheme has better image quantity and higher capacity.
Lacunary Statistical Limit Points in Random 2-Normed Spaces
Authors: Güncan A. , Yamancı U. , Gürdal M.
Published: July 2013

We introduce the notionθ-cluster points, investigate the relation betweenθ-cluster points and limit points of sequences in the topology induced by random 2-normed spaces, and prove some important results.
A Longitudinal Study of the Reliability of Acupuncture Deqi Sensations in Knee Osteoarthritis
Authors: Spaeth Rosa B. , Camhi Stephanie , Hashmi Javeria A. , Vangel Mark , Wasan Ajay D. , Edwards Robert R. , Gollub Randy L. , Kong Jian
Published: July 2013

Deqi is one of the core concepts in acupuncture theory and encompasses a range of sensations. In this study, we used the MGH Acupuncture Sensation Scale (MASS) to measure and assess the reliability of the sensations evoked by acupuncture needle stimulation in a longitudinal clinical trial on knee osteoarthritis (OA) patients. The Knee injury and Osteoarthritis Outcome Score (KOOS) was used as the clinical outcome. Thirty OA patients were randomized into one of three groups (high dose, low dose, and sham acupuncture) for 4 weeks. We found that, compared with sham acupuncture, real acupuncture (combining high and low doses) produced significant improvement in knee pain (P=.025) and function in sport (P=.049). Intraclass correlation analysis showed that patients reliably rated 11 of the 12 acupuncture sensations listed on the MASS and that heaviness was rated most consistently. Overall perceived sensation (MASS Index) (P=.014), ratings of soreness (P=.002), and aching (P=.002) differed significantly across acupuncture groups. Compared to sham acupuncture, real acupuncture reliably evoked stronger deqi sensations and led to better clinical outcomes when measured in a chronic pain population. Our findings highlight the MASS as a useful tool for measuring deqi in acupuncture research.
Supervised Expert System for Wearable MEMS Accelerometer-Based Fall Detector
Authors: Rescio Gabriele , Leone Alessandro , Siciliano Pietro
Published: July 2013

Falling is one of the main causes of trauma, disability, and death among older people. Inertial sensors-based devices are able to detect falls in controlled environments. Often this kind of solution presents poor performances in real conditions. The aim of this work is the development of a computationally low-cost algorithm for feature extraction and the implementation of a machine-learning scheme for people fall detection, by using a triaxial MEMS wearable wireless accelerometer. The proposed approach allows to generalize the detection of fall events in several practical conditions. It appears invariant to the age, weight, height of people, and to the relative positioning area (even in the upper part of the waist), overcoming the drawbacks of well-known threshold-based approaches in which several parameters need to be manually estimated according to the specific features of the end user. In order to limit the workload, the specific study on posture analysis has been avoided, and a polynomial kernel function is used while maintaining high performances in terms of specificity and sensitivity. The supervised clustering step is achieved by implementing an one-class support vector machine classifier in a stand-alone PC.
Convergence of a New Modified Ishikawa Type Iteration for Common Fixed Points of Total Asymptotically Strict Pseudocontractive Semigroups
Authors: Wang Yuanheng , Wang Chunjie
Published: July 2013

The purpose of this paper is to give a new modified Ishikawa type iteration algorithm for common fixed points of total asymptotically strict pseudocontractive semigroups. Under the reduction of some conditions, both strong convergence and weak convergence of the iteration algorithm are proved in Banach spaces with new methods of proofs, respectively. The main results presented in this paper extend and improve the corresponding recent results of many others.
Evaluation of the Effects of Different Surface Configurations on Stability of Miniscrews
Authors: Topcuoglu Tolga , Bicakci A. Altuğ , Avunduk M. Cihat , Sahin Inan Z. Deniz
Published: July 2013

Introduction. The aim of this study was to analyze the effects of screw design and force application on the stability of miniscrews, using RTT, SEM, and histomorphometric analyses. Materials and Methods. Eighty cylindrical, self‐drilling, and Ti6Al4V alloy miniscrews (1,6 × 6 mm) were used. Four mini‐screws were inserted in fibulas of each rabbit, and 115 G of force was immediately applied. Four miniscrews were inserted in the other fibula, on which no force was applied. Eight weeks after insertion, osseointegration between miniscrew and the surrounding bone was evaluated by the histomorphometric analyses, SEM, and RTT. Kruskal‐Wallis and the paired t‐tests were used for statistical analysis. Results. Values obtained from Group I were significantly higher than those of the other loaded groups (P  < .05). There were no differences in RTT scores among Groups II, III, and IV. Similar findings were also observed for unloaded mini‐screws. There was no significant difference between Groups I and IC, while the differences between loaded and unloaded controls for each miniscrew were statistically significant. Conclusions. Immediate loading of miniscrews does not impair screw stability. Also, the diameter of miniscrew and more frequent thread pitches have a positive effect on stability; however, length of miniscrews does not have a significant effect on the stability.
Chinese Herbal Medicine for the Treatment of Prehypertension
Authors: Wang Jie , Feng Bo , Yang Xiaochen , Liu Wei , Xiong Xingjiang
Published: July 2013

Objectives. To assess the current clinical evidence of Chinese herbal medicine (CHM) for prehypertension.Search Strategy. Electronic databases were searched until May, 2013.Inclusion Criteria. We included randomized clinical trials testing CHM against life style intervention and no treatment, or combined with life style intervention against life style intervention.Data Extraction and Analyses. Study selection, data extraction, quality assessment, and data analyses were conducted according to Cochrane standards.Results. Five trials were included. Methodological quality of the trials was evaluated as generally low. Only 1 trial reported allocation sequence. No trial reported the allocation concealment, double blinding, placebo control, presample size estimation, intention to treat analysis, and drop-out. All the included trials were not multicenter and large scale. Although meta-analysis showed that CHM is superior to either life style intervention group or no treatment group in decreasing blood pressure, we are unable to draw a definite conclusion on the effect of CHM due to the poor research methods used in the reviewed trials. The safety of CHM is still uncertain.Conclusions. There is no evidence to show that CHM is effective and safe for prehypertension due to serious methodological flaw of the reviewed trials. Rigorously designed trials are warranted to confirm these results.