Analog property checkers: a DDR2 case study - Jones, Kevin D; Konrad,Victor; Dejan Nickovic (Formal Methods in System Design)
The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be interfaced with a simulator and alert the user if the property is violated by a simulation trace. Although not complete, this lighter approach to formal verification has been effectively used in software and digital hardware to detect errors. Recently, the idea of property checkers has been extended to analog and mixed-signal systems. In this paper, we apply the property-based checking methodology to an industrial and realistic example of a DDR2 memory interface. The properties describing the DDR2 analog behavior are expressed in the formal specification language stl/psl in form of assertions. The simulation traces generated from an actual DDR2 interface design are checked with respect to the stl/psl assertions using the amt tool. The focus of this paper is on the translation of the official (informal and descriptive) specification of two non-trivial DDR2 properties into stl/psl assertions. We study both the benefits and the current limits of such approach.

A marketplace for cloud resources - Henzinger, Thomas A; Tomar, Anmol; Singh, Vasu; Wies, Thomas; Zufferey, Damien
Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context.

FlexPRICE: Flexible provisioning of resources in a cloud environment - Henzinger, Thomas A; Tomar, Anmol; Singh, Vasu; Wies, Thomas; Zufferey, Damien
Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases.

Transactions in the jungle - Guerraoui, Rachid; Henzinger, Thomas A; Kapalka, Michal; Singh, Vasu
Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to the given underlying memory model. We investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of practical relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows developing more efficient TM implementations.

GIST: A solver for probabilistic games - Chatterjee, Krishnendu; Henzinger, Thomas A; Jobstmann, Barbara; Radhakrishna, Arjun
GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.

Robustness of sequential circuits - Doyen, Laurent; Henzinger, Thomas A; Legay, Axel; Nickovic, Dejan
Digital components play a central role in the design of complex embedded systems. These components are interconnected with other, possibly analog, devices and the physical environment. This environment cannot be entirely captured and can provide inaccurate input data to the component. It is thus important for digital components to have a robust behavior, i.e. the presence of a small change in the input sequences should not result in a drastic change in the output sequences. In this paper, we study a notion of robustness for sequential circuits. However, since sequential circuits may have parts that are naturally discontinuous (e.g., digital controllers with switching behavior), we need a flexible framework that accommodates this fact and leaves discontinuous parts of the circuit out from the robustness analysis. As a consequence, we consider sequential circuits that have their input variables partitioned into two disjoint sets: control and disturbance variables. Our contributions are (1) a definition of robustness for sequential circuits as a form of continuity with respect to disturbance variables, (2) the characterization of the exact class of sequential circuits that are robust according to our definition, (3) an algorithm to decide whether a sequential circuit is robust or not.

Model checking of linearizability of concurrent list implementations - Cerny, Pavol; Radhakrishna, Arjun; Zufferey, Damien; Chaudhuri, Swarat; Alur, Rajeev
Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.

Quantitative Simulation Games - Cerny, Pavol; Henzinger, Thomas A; Radhakrishna, Arjun (Time For Verification: Essays in Memory of Amir Pnueli)
While a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a distance function on systems and properties, where the distance between a system and a property provides a measure of “fit” or “desirability.” In this article, we explore several ways how the simulation preorder can be generalized to a distance function. This is done by equipping the classical simulation game between a system and a property with quantitative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness” of the satisfaction, that is, how much the system can deviate from its nominal behavior while still satisfying the property. For systems that violate a property, a quantitative simulation game can measure the “seriousness” of the violation, that is, how much the property has to be modified so that it is satisfied by the system. These distances can be computed in polynomial time, since the computation reduces to the value problem in limit average games with constant weights. Finally, we demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.

Simulation distances - Cerny, Pavol; Henzinger, Thomas A; Radhakrishna, Arjun
Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.

Verifying local transformations on relaxed memory models - Burckhardt, Sebastian; Musuvathi, Madanlal; Singh, Vasu
The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory programs this task is challenging because (1) concurrent threads can observe transformations that would be undetectable in a sequential program, and (2) contemporary multiprocessors commonly use relaxed memory models that complicate the reasoning. In this paper, we present a novel proof methodology for verifying that a local program transformation is sound with respect to a specific hardware memory model, in the sense that it is not observable in any context. The methodology is based on a structural induction and relies on a novel compositional denotational semantics for relaxed memory models that formalizes (1) the behaviors of program fragments as a set of traces, and (2) the effect of memory model relaxations as local trace rewrite operations. To apply this methodology in practice, we implemented a semi- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models.

Shape refinement through explicit heap analysis - Beyer, Dirk; Henzinger, Thomas A; Théoduloz, Grégory; Zufferey, Damien
Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.

The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses - Guetg, Nicole; Seddik, Riad; Vigot, Réjan; Tureček, Rostislav; Gassmann, Martin; Vogt, Kaspar E; Bräuner-Osborne, Hans; Ryuichi Shigemoto; Kretz, Oliver; Frotscher, Michael; Kulik, Ákos; Bettler, Bernhard (Journal of Neuroscience)
GABA B receptor subtypes are based on the subunit isoforms GABA B1a and GABA B1b, which associate with GABA B2 subunits to form pharmacologically indistinguishable GABA B(1a,2) and GABA B(1b,2) receptors. Studies with mice selectively expressing GABA B1a or GABA B1b subunits revealed that GABA B(1a,2) receptors are more abundant than GABA B(1b,2) receptors at glutamatergic terminals. Accordingly, it was found that GABA B(1a,2) receptors are more efficient than GABA B(1b,2) receptors in inhibiting glutamate release when maximally activated by exogenous application of the agonist baclofen. Here, we used a combination of genetic, ultrastructural and electrophysiological approaches to analyze to what extent GABA B(1a,2) and GABA B(1b,2) receptors inhibit glutamate release in response to physiological activation. We first show that at hippocampal mossy fiber (MF)-CA3 pyramidal neuron synapses more GABA B1a than GABA B1b protein is present at presynaptic sites, consistent with the findings at other glutamatergic synapses. In the presence of baclofen at concentrations ≥1 μM, both GABA B(1a,2) and GABA B(1b,2) receptors contribute to presynaptic inhibition of glutamate release. However, at lower concentrations of baclofen, selectively GABA B(1a,2) receptors contribute to presynaptic inhibition. Remarkably, exclusively GABA B(1a,2) receptors inhibit glutamate release in response to synaptically released GABA. Specifically, we demonstrate that selectively GABA B(1a,2) receptors mediate heterosynaptic depression of MF transmission, a physiological phenomenon involving transsynaptic inhibition of glutamate release via presynaptic GABA B receptors. Our data demonstrate that the difference in GABA B1a and GABA B1b protein levels at MF terminals is sufficient to produce a strictly GABA B1a-specific effect under physiological conditions. This consolidates that the differential subcellular localization of the GABA B1a and GABA B1b proteins is of regulatory relevance.

Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold - Jiang, Yuqiang; Horimoto, Noriko N; Imura, Kohei; Matsui, Ko; Ryuichi Shigemoto (Advanced Materials)
The living cell imaging using a two-photon microscope using gold nanoplates and nanoparticle aggregates was demonstrated. The dimensions of the nanoplates were determined through scanning electron microscopy (SEM) and atomic force microscopy. The height of a 100 nm base-length nanotriangle was around 10 nm, while the height of 300 nm base-length nanotriangle was around 12 nm. A spectrophotometer was also used to determine the extinction spectra of gold nanoparticle colloids. Two-photon-induced photoluminescence (TPIPL) under far-field excitation was tested for gold nanoplates on a glass substrate using two-photon laser scanning microscopy (TPLSM). It was observed that living-cell microscopic imaging can be carried out with TPIPL from gold nanoplates and aggregated nanosphere. This method provided a platform for developing tools for biological and biomedical studies.

Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor - Pan, Bingxing; Dong, Yu-Lin; Ito, Wataru; Yanagawa, Yuchio; Ryuichi Shigemoto; Morozov, Alexei A (Neuron)
GABAb receptor (GABAbR)-mediated suppression of glutamate release is critical for limiting glutamatergic transmission across the central nervous system (CNS). Here we show that, upon tetanic stimulation of afferents to lateral amygdala, presynaptic GABAbR-mediated inhibition only occurs in glutamatergic inputs to principle neurons (PNs), not to interneurons (INs), despite the presence of GABAbR in terminals to both types of neurons. The selectivity is caused by differential local GABA accumulation; it requires GABA reuptake and parallels distinct spatial distributions of presynaptic GABAbR in terminals to PNs and INs. Moreover, GABAbR-mediated suppression of theta-burst-induced long-term potentiation (LTP) occurs only in the inputs to PNs, not to INs. Thus, target-cell-specific control of glutamate release by presynaptic GABAbR orchestrates the inhibitory dominance inside amygdala and might contribute to prevention of nonadaptive defensive behaviors.

Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains - Walter Kaufmann; Ferraguti, Francesco; Fukazawa, Yugo; Kasugai, Yu; Ryuichi Shigemoto; Laake, Petter; Sexton, Joseph A; Ruth, Peter; Wietzorrek, Georg; Knaus, Hans G; Storm, Johan F; Ottersen, Ole P (Journal of Comparative Neurology)
Calcium-activated potassium channels have been shown to be critically involved in neuronal function, but an elucidation of their detailed roles awaits identification of the microdomains where they are located. This study was undertaken to unravel the precise subcellular distribution of the large-conductance calcium-activated potassium channels (called BK, KCa1.1, or Slo1) in the somatodendritic compartment of cerebellar Purkinje cells by means of postembedding immunogold cytochemistry and SDS-digested freeze-fracture replica labeling (SDS-FRL). We found BK channels to be unevenly distributed over the Purkinje cell plasma membrane. At distal dendritic compartments, BK channels were scattered over the plasma membrane of dendritic shafts and spines but absent from postsynaptic densities. At the soma and proximal dendrites, BK channels formed two distinct pools. One pool was scattered over the plasma membrane, whereas the other pool was clustered in plasma membrane domains overlying subsurface cisterns. The labeling density ratio of clustered to scattered channels was about 60:1, established in SDS-FRL. Subsurface cisterns, also called hypolemmal cisterns, are subcompartments of the endoplasmic reticulum likely representing calciosomes that unload and refill Ca2+ independently. Purkinje cell subsurface cisterns are enriched in inositol 1,4,5-triphosphate receptors that mediate the effects of several neurotransmitters, hormones, and growth factors by releasing Ca2+ into the cytosol, generating local Ca2+ sparks. Such increases in cytosolic [Ca2+] may be sufficient for BK channel activation. Clustered BK channels in the plasma membrane may thus participate in building a functional unit (plasmerosome) with the underlying calciosome that contributes significantly to local signaling in Purkinje cells.

Mice with altered myelin proteolipid protein gene expression display cognitive deficits accompanied by abnormal neuron-glia interactions and decreased conduction velocities - Tanaka, Hisataka; Ma, Jianmei; Tanaka, Kenji F; Takao, Keizo; Komada, Munekazu; Tanda, Koichi; Suzuki, Ayaka; Ishibashi, Tomoko; Baba, Hiroko; Isa, Tadashi; Ryuichi Shigemoto; Ono, Katsuhiko; et al. (Journal of Neuroscience)
Conduction velocity (CV) of myelinated axons has been shown to be regulated by oligodendrocytes even after myelination has been completed. However, how myelinating oligodendrocytes regulate CV, and what the significance of this regulation is for normal brain function remain unknown. To address these questions, we analyzed a transgenic mouse line harboring extra copies of the myelin proteolipid protein 1 (plp1) gene (plp1tg/- mice) at 2 months of age. At this stage, the plp1tg/- mice have an unaffected myelin structure with a normally appearing ion channel distribution, but the CV in all axonal tracts tested in the CNS is greatly reduced. We also found decreased axonal diameters and slightly abnormal paranodal structures, both of which can be a cause for the reduced CV. Interestingly the plp1tg/- mice showed altered anxiety-like behaviors, reduced prepulse inhibitions, spatial learning deficits and working memory deficit, all of which are schizophrenia-related behaviors. Our results implicate that abnormalities in the neuron-glia interactions at the paranodal junctions can result in reduced CV in the CNS, which then induces behavioral abnormalities related to schizophrenia.

Visual properties of transgenic rats harboring the channelrhodopsin-2 gene regulated by the thy-1.2 promoter - Tomita, Hiroshi; Sugano, Eriko; Fukazawa, Yugo; Isago, Hitomi; Sugiyama, Yuka; Hiroi, Teru; Ishizuka, Toru; Mushiake, Hajime; Kato, Megumi; Hirabayashi, Masumi; Ryuichi Shigemoto; Yawo, Hiromu; et al. (PLoS One)
Channelrhodopsin-2 (ChR2), one of the archea-type rhodopsins from green algae, is a potentially useful optogenetic tool for restoring vision in patients with photoreceptor degeneration, such as retinitis pigmentosa. If the ChR2 gene is transferred to retinal ganglion cells (RGCs), which send visual information to the brain, the RGCs may be repurposed to act as photoreceptors. In this study, by using a transgenic rat expressing ChR2 specifically in the RGCs under the regulation of a Thy-1.2 promoter, we tested the possibility that direct photoactivation of RGCs could restore effective vision. Although the contrast sensitivities of the optomotor responses of transgenic rats were similar to those observed in the wild-type rats, they were enhanced for visual stimuli of low-spatial frequency after the degeneration of native photoreceptors. This result suggests that the visual signals derived from the ChR2-expressing RGCs were reinterpreted by the brain to form behavior-related vision.

Semicircle law on short scales and delocalization of eigenvectors for Wigner random matrices - László Erdös; Schlein, Benjamin; Yau, Horng-Tzer (Annals of Probability)
We consider N×N Hermitian random matrices with i.i.d. entries. The matrix is normalized so that the average spacing between consecutive eigenvalues is of order 1/N. We study the connection between eigenvalue statistics on microscopic energy scales η≪1 and (de)localization properties of the eigenvectors. Under suitable assumptions on the distribution of the single matrix elements, we first give an upper bound on the density of states on short energy scales of order η∼log N/N. We then prove that the density of states concentrates around the Wigner semicircle law on energy scales η≫N−2/3. We show that most eigenvectors are fully delocalized in the sense that their ℓp-norms are comparable with N1/p−1/2 for p≥2, and we obtain the weaker bound N2/3(1/p−1/2) for all eigenvectors whose eigenvalues are separated away from the spectral edges. We also prove that, with a probability very close to one, no eigenvector can be localized. Finally, we give an optimal bound on the second moment of the Green function.

Quantum dynamics with mean field interactions: A new approach - László Erdös; Schlein, Benjamin (Journal of Statistical Physics)
We propose a new approach for the study of the time evolution of a factorized N-particle bosonic wave function with respect to a mean-field dynamics with a bounded interaction potential. The new technique, which is based on the control of the growth of the correlations among the particles, leads to quantitative bounds on the difference between the many-particle Schrödinger dynamics and the one-particle nonlinear Hartree dynamics. In particular the one-particle density matrix associated with the solution to the N-particle Schrödinger equation is shown to converge to the projection onto the one-dimensional sub-space spanned by the solution to the Hartree equation with a speed of convergence of order 1/N for all fixed times.

Local semicircle law and complete delocalization for Wigner random matrices - László Erdös; Schlein, Benjamin; Yau, Horng-Tzer (Communications in Mathematical Physics)
We consider N × N Hermitian random matrices with independent identical distributed entries. The matrix is normalized so that the average spacing between consecutive eigenvalues is of order 1/N. Under suitable assumptions on the distribution of the single matrix element, we prove that, away from the spectral edges, the density of eigenvalues concentrates around the Wigner semicircle law on energy scales n ≫ N -1 (log N) 8 . Up to the logarithmic factor, this is the smallest energy scale for which the semicircle law may be valid. We also prove that for all eigenvalues away from the spectral edges, the -tempℓ∞-norm of the corresponding eigenvectors is of order O(N -1/2), modulo logarithmic corrections. The upper bound O(N -1/2) implies that every eigenvector is completely delocalized, i.e., the maximum size of the components of the eigenvector is of the same order as their average size. In the Appendix, we include a lemma by J. Bourgain which removes one of our assumptions on the distribution of the matrix elements.