Browsing by Subject "Synchronization"
Now showing 1 - 15 of 15
Results Per Page
Sort Options
Item Asynchronous automatic-signal monitors with multi-object synchronization(2016-12) Hung, Wei-Lun; Garg, Vijay K. (Vijay Kumar), 1963-; Julien, Christine; Khurshid, Sarfraz; Mittal, Neeraj; Perry, Dewayne E; Pingali, KeshavOne of the fundamental problems in parallel programming is that there is no simple programming paradigm that provides mutual exclusion and synchronization with efficient implementation at the same time. For monitor [Hoa74,Han75] (lock-based) systems, only experienced programmers can develop high-performance fine-grained lock-based implementations. Programmers frequently introduce bugs with traditional monitors. Researchers have proposed transactional memory [HM93,ST95], which provides a simple and elegant mechanism for programmers to atomically execute a set of memory operations so that there is no deadlock in transactional memory systems. However, most of transactional memory systems lack conditional synchronization support [WLS14,LW14]. Hence, writing multi-threaded programs with conditional synchronization is rather difficult. In this dissertation, we develop a parallel programming framework that provides simple constructs for mutual exclusion and synchronization as well as efficient implementation.Item Cardiorespiratory synchronization, a mathematical model(2008-12) Hensley, Nicholas; Martin, Clyde F.; Ghosh, Bijoy K.This thesis examines the relationship of the human cardiovascular system and the human respiratory system. It is understood that these systems experience synchronization. In other words, the heart rate and the respiratory rate often vary concurrently. For example, during exercise, the heart rate and the respiratory rate increase simultaneously. Numerous examples of mathematical models of this phenomenon are found in previous research. Some utilize a large body of equations to describe the many aspects that affect this relationship. In this research, Van der Pol equations are introduced as models of thecardiovascular system and the respiratory system. The proposed model is then analyzed in MATLAB and examined for certain desired properties. Ultimately, a controller emulating the central chemoreceptors of the brain is included in this model. This model allows for the variation of the amplitude and the frequency of the oscillators and the levels of carbon dioxide and oxygen within the blood. The resulting model allows for observation of behaviors of cardiorespiratory synchronization during different levels of carbon dioxide deficiency and oxygen deficiency. Therefore, the model may be used to draw certain conclusions about how the human body responds to different conditions such as hypocapnia and hypercapnia.Item Communication Reliability in Network on Chip Designs(2012-10-19) Kumar, ReeshavThe performance of low latency Network on Chip (NoC) architectures, which incorporate fast bypass paths to reduce communication latency, is limited by crosstalk induced skewing of signal transitions on link wires. As a result of crosstalk interactions between wires, signal transitions belonging to the same flit or bit vector arrive at the destination at different times and are likely to violate setup and hold time constraints for the design. This thesis proposes a two-step technique: TransSync- RecSync, to dynamically eliminate packet errors resulting from inter-bit-line transition skew. The proposed approach adds minimally to router complexity and involves no wire overhead. The actual throughput of NoC designs with asynchronous bypass designs is evaluated and the benefits of augmenting such schemes with the proposed design are studied. The TransSync, TransSync-2-lines and RecSync schemes described here are found to improve the average communication latency by 26%, 20% and 38% respectively in a 7X7 mesh NoC with asynchronous bypass channel. This work also evaluates the bit-error ratio (BER) performance of several existing crosstalk avoidance and error correcting schemes and compares them to that of the proposed schemes. Both TransSync and RecSync scheme are dynamic in nature and can be switched on and off on-the-fly. The proposed schemes can therefore be employed to impart unequal error protection (UEP) against intra-flit skewing on NoC links. In the UEP, a larger fraction of the energy budget is spent in providing protection to those parts of the data being transmitted on the link which have a higher priority, while expending smaller effort in protecting relatively less important parts of the data. This allows us to achieve the prescribed level of performance with lower levels of power. The benefits of the presented technique are illustrated using an H.264 video decoder system-on-chip (SoC) employing NoC architecture. We show that for Akyio test streams transmitted over 3mm long link wires, the power consumption can be reduced by as much as 20% at the cost of an acceptable degradation in average peak signal to noise ratio (PSNR) with UEP.Item Design and Implementation of Physical Layer Network Coding Protocols(2010-10-12) Maduike, Dumezie K.There has recently been growing interest in using physical layer network coding techniques to facilitate information transfer in wireless relay networks. The physical layer network coding technique takes advantage of the additive nature of wireless signals by allowing two terminals to transmit simultaneously to the relay node. This technique has several performance benefits, such as improving utilization and throughput of wireless channels and reducing delay. In this thesis, we present an algorithm for joint decoding of two unsynchronized transmitters to a modulo-2 sum of their transmitted messages. We address the problems that arise when the boundaries of the signals do not align with each other and when their phases are not identical. Our approach uses a state-based Viterbi decoding scheme that takes into account the timing offsets between the interfering signals. As a future research plan, we plan to utilize software-defined radios (SDRs) as a testbed to show the practicality of our approach and to verify its performance. Our simulation studies show that the decoder performs well with the only degrading factor being the noise level in the channel.Item Design of a clock synchronization circuit(Texas Tech University, 2001-08) Elahi, Noor-EWith the advent of digital networks and the transmission and reception of binary pulses (Is and Os), it became important to devise some method for detecting these signals accurately at the receiver. The ideal system is one in which the binary pulses arrive at the receiver in a very precise and concise manner. This means that the receiver knows the exact time when the signal (a binary 1 or 0) manifests itself at the receiver interface. Fortunately, it is relatively easy to determine this timing, because the receiver can derive the clock from the incoming bit stream by examining when the pulses arrive at the receiver. This function is called cock recovery. The rest ofthe data can be detected using this clock. However, errors can occur if the clock is not aligned with the signal or data. This leads to wrong information in the receiver about the timing of received data. This problem is usually called phase variation, and may translate into an incorrect interpretation of the binary Is and Os in the transmission stream. So it is vital for digital transmission that the data transmitted should be aligned to a pure clock, which has no phase variations. As shown in Figure 1.1, the signal and the clock are perfectly aligned to a clock with no phase variations. The positive edge ofthe clock is at the middle of each 1 or 0. This clock is referred to as a reference clock.Item Heart rate entrainment to external auditory rhythm: A pilot study(2017-04-18) Way, Michael Harrison; Dachinger, Carolyn; Miller, Karen; Henderson, CraigHeart rate entrainment to external auditory rhythm has numerous applications to clinical music therapy practice, including increasing arousal or inducing relaxation. However, research regarding the ability of heart rate to entrain to external auditory stimuli is contradictory or incomplete, leading to questions regarding this phenomenon. Thus, the current study was conducted to investigate if heart rate can entrain to external auditory stimuli. Eighty-four participants were randomly placed into three testing groups. The baseline heart rate of each participant was measured over a 5 minute period, then, depending on the group, 7%, 10% or 15% was subtracted from the baseline to get the target heart rate. An external auditory stimulus was then played at the target rate for a 15 minute period while heart rate was continuously monitored. Results indicated that there is a possibility of heart rate entrainment at the 7% and 10% level, with statistically significant differences observed between the 7% and 10% groups as well as the 7% and 15% groups. These results align with ideas from previous research and can act as the groundwork for future research exploring heart rate entrainment to other forms of auditory stimuli. The findings from this research could also be used to help music therapists select tempi that are appropriate for relaxation interventions. These findings could also be used for additional research investigating the use of heart rate entrainment as a physiological indicator of consciousness in patients under the disorders of consciousness umbrella.Item Improved algorithms and hardware designs for division by convergence(2009-12) Kong, Inwook; Swartzlander, Earl E.This dissertation focuses on improving the division-by-convergence algorithm. While the division by convergence algorithm has many advantages, it has some drawbacks, such as a need for extra bits in the multiplier and a large ROM table for the initial approximation. To mitigate these problems, two new methods are proposed here. In addition, the research scope is extended to seek an efficient architecture for implementing a divider with Quantum-dot Cellular Automata (QCA), an emerging technology. For the first proposed approach, a new rounding method to reduce the required precision of the multiplier for division by convergence is presented. It allows twice the error tolerance of conventional methods and inclusive error bounds. The proposed method further reduces the required precision of the multiplier by considering the asymmetric error bounds of Goldschmidt dividers. The second proposed approach is a method to increase the speed of convergence for Goldschmidt division using simple logic circuits. The proposed method achieves nearly cubic convergence. It reduces the logic complexity and delay by using an approximate squarer with a simple logic implementation and a redundant binary Booth recoder. Finally, a new architecture for division-by-convergence in QCA is proposed. State machines for QCA often have synchronization problems due to the long wire delays. To resolve this problem, a data tag method is proposed. It also increases the throughput significantly since multiple division computations can be performed in a time skewed manner using one iterative divider.Item Investigation for analog phase locked loop jitter phenomenon(Texas Tech University, 2002-05) Chung, Ming YauNot availableItem Pre- and post-synchronization methodologies to enhance the efficiency of fixed timed artificial insemination in pharmacologically-controlled breeding systems with Bos indicus-influenced cattle(Texas A&M University, 2007-04-25) Zuluaga Velez, Juan FedericoObjectives were to: 1) Evaluate the effectiveness of presynchronization with GnRH before the CO??????Synch + CIDR protocol with timed AI (TAI) at 66 h in Bos indicus??????influenced cattle; 2) Characterize ovarian events associated with the presynchronization; 3) Evaluate the efficacy of measuring vaginal electrical resistance (VER) to assess follicular maturity at TAI; and 4) Compare serum concentrations of progesterone (P4) in ovariectomized cows bearing new or previously used CIDR devices with or without autoclaving. In Exp. 1 and 2, cattle received either GnRH or saline on day ??????7. The CO??????Synch + CIDR protocol included a CIDR insert and GnRH (GnRH??????1; day 0), removal of CIDR and PGF2???? on day 7, and GnRH (GnRH??????2) and TAI 66 h after CIDR removal. In Exp. 1, pregnancy rate of females with BCS ?????? 5 tended to differ (P=0.085) between Presynch (38%) and CO??????Synch + CIDR (54%). In Exp. 2, ovulatory response to GnRH??????1 was greater (P<0.01) in the Presynchronization (58%) than in the CO??????Synch + CIDR (27.1%) group. Emergence of a follicular wave after GnRH??????1 and ovulation rate after GnRH??????2 did not differ between groups. More (P<0.01) females that developed a follicular wave after GnRH??????1 ovulated (82%) after GnRH??????2, compared to those that did not (29%). Mean VER (ohms) was greatest (101.4????0.8) on day 0 and declined (P<0.01) to 95.2????0.8 and 82????0.8, respectively, on days 7 and 10. We observed a low negative but significant relationship (r=0.38; P<0.001) between VER and follicular size on day 0, 7, and 10. VER difference (day 10 minus day 7) did not differ between females with small and large follicles at TAI. Mean concentrations of P4 during the 7??????day insertion period were greater (P<0.03) for new (3.7 ng/ml) and re??????used autoclaved (3.4 ng/ml) than for re??????used disinfected CIDRs (2.8 ng/ml). In summary, Presynch improved ovulation rate after GnRH??????1, but did not improve pregnancy rates compared to CO??????Synch + CIDR. Follicular maturity estimation was not feasible using VER as applied in this study. Autoclaving may be the best option when re??????using CIDR inserts because it creates greater concentrations of P4 during the first 48 h.Item Regulation and Synchronization of the Master Circadian Clock by Purinergic Signaling from Suprachiasmatic Nucleus Astrocytes(2012-10-19) Womac, Alisa DianeMolecular, cellular, and physiological processes within an organism are set to occur at specific times throughout the day. The timing of these processes is under control of a biological clock. Nearly all organisms on Earth have biological clocks, ranging from unicellular bacteria and fungi to multicellular plants, insects, reptiles, fish, birds, and mammals. The biological clock is an endogenous time-keeping mechanism that generates the onset of many processes and coordinates the phases of processes over 24 hours. While the biological clock allows these organisms to maintain roughly 24-hour, or circadian, timing in daily processes, many organisms have the ability to set their clocks, or entrain them, to changes in light. In mammals, the suprachiasmatic nucleus (SCN) is the master biological clock that entrains daily physiological and behavioral rhythms to the appropriate times of day and night. The SCN is located in the hypothalamus and contains thousands of neurons and glia that function in coordinating system-level physiological rhythms that are entrained to environmental light cues. Many of these neurons and glia are individual circadian oscillators, and the cellular mechanisms that couple them into ensemble oscillations are emerging. Adenosine triphosphate (ATP) is a transmitter involved in local communication among astrocytes and between astrocytes and neurons. ATP released from astrocytes may play a role in SCN cellular communication and synchrony. Extracellular ATP accumulated rhythmically in the rat SCN in vivo, and ATP released from rat SCN astrocytes in vitro was rhythmic, with a periodicity near 24 hours. ATP released from mouse SCN astrocytes was circadian, and disruption of the molecular clock abolished rhythmic extracellular ATP accumulation. SCN astrocyte cultures with disrupted molecular clocks also had marked reductions in total ATP accumulation compared to SCN astrocyte cultures with functional biological clocks. Furthermore, ATP-induced calcium transients were rhythmic, and this rhythmic purinergic sensitivity was abolished in clock mutant astrocytes. Pharmacological blockade of purinergic signaling, with antagonists of both the P2X7 and P2Y1 receptors, led to a gradual reduction in the amplitude of coordinated ATP accumulation over three days. These purinergic receptor antagonists, as expected, led to a reduction in calcium responses of SCN astrocytes to ATP and led to a dampening of clock gene expression rhythms as determined by PER2::LUC bioluminescence reporting in SCN astrocytes. These data demonstrate that astrocytes of the mammalian SCN rhythmically release ATP and are rhythmically sensitive to ATP in a manner dependent on their intrinsic molecular clock. Ensemble rhythmicity of SCN astrocytes is, in turn, dependent on that rhythmic purinergic signaling via both P2X and P2Y classes of ATP receptors. These results are indicative of a functional role for ATP accumulation within the SCN, with astrocytes releasing ATP every 24 hours for continual signaling onto astrocytes and neurons to maintain daily coordinated synchrony of the clocks in these cells.Item Sensitivity of OFDM Systems to Synchronization Errors and Spatial Diversity(2012-02-14) Zhou, YiIn this dissertation, the problem of synchronization for OFDM-based wireless communication systems is studied. In the first part of this dissertation, the sensitivity of both single input single output (SISO) OFDM and multiple input multiple output (MIMO) OFDM receivers to carrier and timing synchronization errors are analyzed. Analytical expressions and numerical results for the power of inter-carrier interference (ICI) are presented. It is shown that the OFDM-based receivers are quite sensitive to residual synchronization errors. In wide-sense stationary uncorrelated scattering (WSSUS) frequency-selective fading channels, the sampling clock timing offset results in rotation of the subcarrier constellation, while carrier frequency offsets and phase jitter cause inter-carrier interference. The overall system performance in terms of symbol error rate is limited by the inter-carrier interference. For a reliable information reception, compensatory measures must be taken. The second part of this dissertation deals with the impact of spatial diversity (usage of multiple transmit/receive antennas) on synchronization. It is found that with multiple transmit and receive antennas, MIMO-OFDM systems can take advantage of the spatial diversity to combat carrier and timing synchronization imperfections. Diversity can favorably improve the synchronization performance. Data-aided and non-data-aided maximum likelihood symbol timing estimators for MIMO-OFDM systems are introduced. Computer simulations show that, by exploiting the spatial diversity, synchronization performance of MIMO-OFDM systems in terms of mean squared error (MSE) of residual timing offset becomes significantly more reliable when compared to conventional SISO OFDM systems. Therefore, spatial diversity is a useful technique to be exploited in the deployment of MIMO-OFDM communication systems. In MIMO systems with synchronization sequences, timing synchronization is treated as a multiple hypotheses testing problem. Generalized likelihood ratio test (GLRT) statistics are developed for MIMO systems in frequency flat channels and MIMO-OFDM systems in frequency selective fading environments. The asymptotic performance of the GLRT without nuisance parameters is carried out. It is shown that the asymptotic performance of the GLRT can serve as an upper bound for the detection probability in the presence of a limited number of observations as well as a benchmark for comparing the performances of different timing synchronizers.Item Synchronization of Mechanical Oscillators: An Experimental Study(2011-02-22) Daneshvar, RoozbehIn this research we consider synchronization of oscillators. We use mechanical metronomes that are coupled through a mechanical medium. We investigate the problem for three different cases: 1) In passive coupling of two oscillators, the coupling medium is a one degree of freedom passive mechanical basis. The analysis of the system is supported by simulations of the proposed model and experimental results. 2) In another case, the oscillator is forced by an external input while the input is also affected by the oscillator. This feedback loop introduces dynamics to the whole system. For realization, we place the mechanical metronome on a one degree of freedom moving base. The movements of the base are a function of a feedback from the phase of the metronome. We study a family of functions for the reactions of the base and their impact on the behavior of the metronome. 3) We consider two metronomes located on a moving base. In this case the two metronomes oscillate and as the base is not freely moving, they are not directly coupled to each other. Now based on the feedbacks from the vision system, the base moves and hence the phases of the metronomes are affected by these movements. We study the space of possibilities for the movements of the base and consider impacts of the base movement on the synchronization of metronomes. We also show how such a system evolves in time.Item The Coordianted Decentralized Paratransit Sysyem: Design, Formulation, and Heuristic(2012-07-16) Shen, Chung-WeiThis dissertation investigates the different organizational structures of paratransit services that cover large regions. A paratransit service is demand-responsive, shared-ride transit service using vans or small buses. It is characterized by the use of vehicles that do not operate on a fixed route or a fixed schedule. The paratransit route and schedule are arranged from a user-specified origin to a user-specified destination, and at a user-specified time. To retain productivity by focusing on shorter trips within a denser area, some larger systems have outsourced operations to more than one contractor, with each contractor responsible for the service zone to which their vehicles have been assigned. This service design is called a "zonal structure" or a "zoning approach." The zoning with transfer system coordinates vehicles' schedules at various transfer locations. The schedule coordination of inter-zonal mechanisms of transportation likely reduces trip costs by increasing the ridesharing rate and lowering the number of empty return miles. This study first presents the exact formulation for a coordinated decentralized paratransit system in order to compare its productivity and service quality with independent decentralized and centralized strategies. The formulation is then proven to work correctly, and the results of the computational experiments of small scale instances are shown to demonstrate that the proposed coordinated system is superior to independent decentralized systems in terms of passenger miles per vehicle revenue mile. In the second section, this study develops an insertion-based heuristic method in order to compare the performances of different operational designs when applied to a large-scale system. In an experiment utilizing Houston's demand-responsive service data, we compare the productivity and service levels among three organizational structures: zoning with transfer, zoning without transfer, and no-zoning designs. The results indicate that zoning with transfer can provide significant benefits to paratransit operations that manage zoning structure; however, the no-zoning strategy used by Houston METRO (a relatively low-density region) performs better on average in terms of efficiency. This study concludes that the zoning with transfer method can be proven to be a productive organizational structure.Item Transparent replication(2006) Nayate, Amol Pramod; Dahlin, MikeIncreasing user expectations and demands have caused the evolution of web services away from single-server systems and toward distributed systems for their ability to provide improved throughput, improved availability and reduced response times. However, for a service to run on a distributed system, each running instance must be able to access data that are shared among the instances. Although existing off-the-shelf replication systems - e.g. distributed file systems [52, 61, 32, 38, 41], replicated databases [64, 75], distributed hash tables [58, 59, 63, 34], etc. - simplify access to shared data by exporting wellresearched interfaces, their implementations are typically not engineered for the unique environments presented by many web services. For example, replication systems that require synchronization across multiple nodes to handle modified data [38, 12] or systems that require all nodes to keep a copy of all data [64, 75] may not be practical for use in such services. Although the problem of general replication is not possible to solve [11, 62, 33] we focus our study on a class of single-writer services that we denote Information Dissemination Services that form a restrictive but important set of web services. Our research makes two key contributions. First, we show that for a class of single-writer services that we denote Information Dissemation Services TRIP replicates dynamic data in a manner that is nearly transparent to the service. We (1) develop a novel dual-channel replication algorithm for TRIP that utilizes spare network background traffic to speculatively replicate data in a safe, non-interfering fashion, (2) show how to integrate safe speculative replication with mechanisms that use invalidates to provide consistency, and (3) demonstrate how our combination of consistency and safe speculative replication allows us to provide near-ideal consistency, performance, and availability for Information Dissemination Services. Second, we show that the core principles behind building TRIP can be extended to build a new replication framework and more general replication toolkit. In particular, we show that it is possible to extend our dual-queue mechanisms developed for TRIP to a multi-writer environment where nodes can synchronize multiple incoming streams of data and consistency information. Our extension allows providing various forms of consistency for arbitrary topologies - two key properties provided by the PRACTI [6] (Partial Replication, Arbitrary Consistency, Topology Independence) architecture.Item Verification of sequential and concurrent libraries(2010-08) Deshmukh, Jyotirmoy Vinay; Emerson, E. Allen; Aziz, Adnan; Garg, Vijay K.; Chase, Craig M.; Khurshid, Sarfraz; Mok, Aloysius K.The goal of this dissertation is to present new and improved techniques for fully automatic verification of sequential and concurrent software libraries. In most cases, automatic software verification is plagued by undecidability, while in many others it suffers from prohibitively high computational complexity. Model checking -- a highly successful technique used for verifying finite state hardware circuits against logical specifications -- has been less widely adapted for software, as software verification tends to involve reasoning about potentially infinite state-spaces. Two of the biggest culprits responsible for making software model checking hard are heap-allocated data structures and concurrency. In the first part of this dissertation, we study the problem of verifying shape properties of sequential data structure libraries. Such libraries are implemented as collections of methods that manipulate the underlying data structure. Examples of such methods include: methods to insert, delete, and update data values of nodes in linked lists, binary trees, and directed acyclic graphs; methods to reverse linked lists; and methods to rotate balanced trees. Well-written methods are accompanied by documentation that specifies the observational behavior of these methods in terms of pre/post-conditions. A pre-condition [phi] for a method M characterizes the state of a data structure before the method acts on it, and the post-condition [psi] characterizes the state of the data structure after the method has terminated. In a certain sense, we can view the method as a function that operates on an input data structure, producing an output data structure. Examples of such pre/post-conditions include shape properties such as acyclicity, sorted-ness, tree-ness, reachability of particular data values, and reachability of pointer values, and data structure-specific properties such as: "no red node has a red child'', and "there is no node with data value 'a' in the data structure''. Moreover, methods are often expected not to violate certain safety properties such as the absence of dangling pointers, absence of null pointer dereferences, and absence of memory leaks. We often assume such specifications as implicit, and say that a method is incorrect if it violates such specifications. We model data structures as directed graphs, and use the two terms interchangeably. Verifying correctness of methods operating on graphs is an instance of the parameterized verification problem: for every input graph that satisfies [phi], we wish to ensure that the corresponding output graph satisfies [psi]. Control structures such as loops and recursion allow an arbitrary method to simulate a Turing Machine. Hence, the parameterized verification problem for arbitrary methods is undecidable. One of the main contributions of this dissertation is in identifying mathematical conditions on a programming language fragment for which parameterized verification is not only decidable, but also efficient from a complexity perspective. The decidable fragment we consider can be broadly sub-divided into two categories: the class of iterative methods, or methods which use loops as a control flow construct to traverse a data structure, and the class of recursive methods, or methods that use recursion to traverse the data structure. We show that for an iterative method operating on a directed graph, if we are guaranteed that if the number of destructive updates that a method performs is bounded (by a constant, i.e., O(1)), and is guaranteed to terminate, then the correctness of the method can be checked in time polynomial in the size of the method and its specifications. Further, we provide a well-defined syntactic fragment for recursive methods operating on tree-like data structures, which assures that any method in this fragment can be verified in time polynomial in the size of the method and its specifications. Our approach draws on the theory of tree automata, and we show that parameterized correctness can be reduced to emptiness of finite-state, nondeterministic tree automata that operate on infinite trees. We then leverage efficient algorithms for checking the emptiness of such tree automata to obtain a tractable verification framework. Our prototype tool demonstrates the low theoretical complexity of our technique by efficiently verifying common methods that operate on data structures. In the second part of the dissertation, we tackle another obstacle for tractable software verification: concurrency. In particular, we explore application of a static analysis technique based on interprocedural dataflow analysis to predict and document deadlocks in concurrent libraries, and analyze deadlocks in clients that use such libraries. The kind of deadlocks that we focus result from circular dependencies in the acquisition of shared resources (such as locks). Well-written applications that use several locks implicitly assume a certain partial order in which locks are acquired by threads. A cycle in the lock acquisition order is an indicator of a possible deadlock within the application. Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in a manner that violates the partial ordering between lock acquisitions that is implicit within the library. Given a concurrent library, we present a technique for inferring interface contracts that speciy permissible concurrent method calls and patterns of aliasing among method arguments that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a satisfiability modulo theories (SMT) solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signalling primitives such as wait-notify for cooperative synchronization. We demonstrate its scalability and efficiency with a prototype tool that analyzed over a million lines of code for some widely-used open-source Java libraries in less than 50 minutes. Furthermore, the contracts inferred by our approach have been able to pinpoint real bugs, i.e. deadlocks that have been reported by users of these libraries.