-
Locksynth: Deriving Synchronization Code for Concurrent Data Structures with ASP
Authors:
Sarat Chandra Varanasi,
Neeraj Mittal,
Gopal Gupta
Abstract:
We present Locksynth, a tool that automatically derives synchronization needed for destructive updates to concurrent data structures that involve a constant number of shared heap memory write operations. Locksynth serves as the implementation of our prior work on deriving abstract synchronization code. Designing concurrent data structures involves inferring correct synchronization code starting wi…
▽ More
We present Locksynth, a tool that automatically derives synchronization needed for destructive updates to concurrent data structures that involve a constant number of shared heap memory write operations. Locksynth serves as the implementation of our prior work on deriving abstract synchronization code. Designing concurrent data structures involves inferring correct synchronization code starting with a prior understanding of the sequential data structure's operations. Further, an understanding of shared memory model and the synchronization primitives is also required. The reasoning involved transforming a sequential data structure into its concurrent version can be performed using Answer Set Programming and we mechanized our approach in previous work. The reasoning involves deduction and abduction that can be succinctly modeled in ASP. We assume that the abstract sequential code of the data structure's operations is provided, alongside axioms that describe concurrent behavior. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees that involve a constant number of destructive update operations. We also are able to infer the correct set of locks (but not code synthesis) for external height-balanced binary search trees that involve left/right tree rotations. Locksynth performs the analyses required to infer correct sets of locks and as a final step, also derives the C++ synchronization code for the synthesized data structures. We also provide a performance analysis of the C++ code synthesized by Locksynth with the hand-crafted versions available from the Synchrobench microbenchmark suite. To the best of our knowledge, our tool is the first to employ ASP as a backend reasoner to perform concurrent data structure synthesis.
△ Less
Submitted 20 May, 2023;
originally announced May 2023.
-
Automating UAV Flight Readiness Approval using Goal-Directed Answer Set Programming
Authors:
Sarat Chandra Varanasi,
Baoluo Meng,
Christopher Alexander,
Szabolcs Borgyos,
Brendan Hall
Abstract:
We present a novel application of Goal-Directed Answer Set Programming that digitizes the model aircraft operator's compliance verification against the Academy of Model Aircrafts (AMA) safety code. The AMA safety code regulates how AMA flyers operate Unmanned Aerial Vehicles (UAVs) for limited recreational purposes. Flying drones and their operators are subject to various rules before and after th…
▽ More
We present a novel application of Goal-Directed Answer Set Programming that digitizes the model aircraft operator's compliance verification against the Academy of Model Aircrafts (AMA) safety code. The AMA safety code regulates how AMA flyers operate Unmanned Aerial Vehicles (UAVs) for limited recreational purposes. Flying drones and their operators are subject to various rules before and after the operation of the aircraft to ensure safe flights. In this paper, we leverage Answer Set Programming to encode the AMA safety code and automate compliance checks. To check compliance, we use the s(CASP) which is a goal-directed ASP engine. By using s(CASP) the operators can easily check for violations and obtain a justification tree explaining the cause of the violations in human-readable natural language. Further, we implement an algorithm to help the operators obtain the minimal set of conditions that need to be satisfied in order to pass the compliance check. We develop a front-end questionnaire interface that accepts various conditions and use the backend s(CASP) engine to evaluate whether the conditions adhere to the regulations. We also leverage s(CASP) implemented in SWI-Prolog, where SWI-Prolog exposes the reasoning capabilities of s(CASP) as a REST service. To the best of our knowledge, this is the first application of ASP in the AMA and Avionics Compliance and Certification space.
△ Less
Submitted 25 August, 2022;
originally announced August 2022.
-
Effect of Succinonitrile on Ion Transport in PEO-based Lithium Ion Battery Electrolytes
Authors:
Sipra Mohapatra,
Shubham Sharma,
Aman Sriperumbuduru,
Srinivasa Rao Varanasi,
Santosh Mogurampelly
Abstract:
We report the ion transport mechanisms in succinonitrile (SN) loaded solid polymer electrolytes containing polyethylene oxide (PEO) and dissolved lithium bis(trifluoromethane)sulphonamide (LiTFSI) salt using molecular dynamics simulations. We investigated the effect of temperature and loading of SN on ion transport and relaxation phenomenon in PEO-LiTFSI electrolytes. It is observed that SN increa…
▽ More
We report the ion transport mechanisms in succinonitrile (SN) loaded solid polymer electrolytes containing polyethylene oxide (PEO) and dissolved lithium bis(trifluoromethane)sulphonamide (LiTFSI) salt using molecular dynamics simulations. We investigated the effect of temperature and loading of SN on ion transport and relaxation phenomenon in PEO-LiTFSI electrolytes. It is observed that SN increases the ionic diffusivities in PEO-based solid polymer electrolytes and makes them suitable for battery applications. Interestingly, the diffusion coefficient of TFSI ions is an order of magnitude higher than the diffusion coefficient of lithium ions across the range of temperatures and loadings integrated. By analyzing different relaxation timescales and examining the underlying transport mechanisms in SN-loaded systems, we find that the diffusivity of TFSI ions correlates excellently with the Li-TFSI ion-pair relaxation timescales. In contrast, our simulations predict distinct transport mechanisms for Li-ions in SN-loaded PEO-LiTFSI electrolytes. Explicitly, the diffusivity of lithium ions cannot be uniquely determined by the ion-pair relaxation timescales but additionally depends on the polymer segmental dynamics. On the other hand, the SN loading induced diffusion coefficient at a given temperature does not correlate with either the ion-pair relaxation timescales or the polymer segmental relaxation timescales.
△ Less
Submitted 11 May, 2022; v1 submitted 12 December, 2021;
originally announced December 2021.
-
CASPR: A Commonsense Reasoning-based Conversational Socialbot
Authors:
Kinjal Basu,
Huaduo Wang,
Nancy Dominguez,
Xiangci Li,
Fang Li,
Sarat Chandra Varanasi,
Gopal Gupta
Abstract:
We report on the design and development of the CASPR system, a socialbot designed to compete in the Amazon Alexa Socialbot Challenge 4. CASPR's distinguishing characteristic is that it will use automated commonsense reasoning to truly "understand" dialogs, allowing it to converse like a human. Three main requirements of a socialbot are that it should be able to "understand" users' utterances, poss…
▽ More
We report on the design and development of the CASPR system, a socialbot designed to compete in the Amazon Alexa Socialbot Challenge 4. CASPR's distinguishing characteristic is that it will use automated commonsense reasoning to truly "understand" dialogs, allowing it to converse like a human. Three main requirements of a socialbot are that it should be able to "understand" users' utterances, possess a strategy for holding a conversation, and be able to learn new knowledge. We developed techniques such as conversational knowledge template (CKT) to approximate commonsense reasoning needed to hold a conversation on specific topics. We present the philosophy behind CASPR's design as well as details of its implementation. We also report on CASPR's performance as well as discuss lessons learned.
△ Less
Submitted 11 October, 2021;
originally announced October 2021.
-
Hydrogen and deuterium charging of site-specific specimen for atom probe tomography
Authors:
Heena Khanchandani,
Se-Ho Kim,
Rama Srinivas Varanasi,
TS Prithiv,
Leigh T. Stephenson,
Baptiste Gault
Abstract:
Hydrogen embrittlement can cause a dramatic deterioration of the mechanical properties of high-strength metallic materials. Despite decades of experimental and modelling studies, the exact underlying mechanisms behind hydrogen embrittlement remain elusive. To unlock understanding of the mechanism and thereby help mitigate the influence of hydrogen and the associated embrittlement, it is essential…
▽ More
Hydrogen embrittlement can cause a dramatic deterioration of the mechanical properties of high-strength metallic materials. Despite decades of experimental and modelling studies, the exact underlying mechanisms behind hydrogen embrittlement remain elusive. To unlock understanding of the mechanism and thereby help mitigate the influence of hydrogen and the associated embrittlement, it is essential to examine the interactions of hydrogen with structural defects such as grain boundaries, dislocations and stacking faults. Atom probe tomography (APT) can, in principle, analyse hydrogen located specifically at such microstructural features but faces strong challenges when it comes to charging specimens with hydrogen or deuterium. Here, we describe three different workflows enabling hydrogen/deuterium charging of site-specific APT specimens: namely cathodic, plasma and gas charging. We discuss in detail the caveats of the different approaches in order to help with future research efforts and facilitate further studies of hydrogen in metals. Our study demonstrates successful cathodic and gas charging, with the latter being more promising for the analysis of the high-strength steels at the core of our work.
△ Less
Submitted 28 September, 2021;
originally announced September 2021.
-
Generating Concurrent Programs From Sequential Data Structure Knowledge Using Answer Set Programming
Authors:
Sarat Chandra Varanasi,
Neeraj Mittal,
Gopal Gupta
Abstract:
We tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requir…
▽ More
We tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using automated commonsense reasoning. We assume that the data structure description is provided as axioms alongside the sequential code of its algebraic operations. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees. Knowledge in our case is expressed using Answer Set Programming (ASP), and we employ deduction and abduction -- just as humans do -- in the reasoning involved. ASP allows for succinct modeling of first order theories of pointer data structures, run-time thread interactions and shared memory synchronization. Our reasoner can systematically make the same judgments as a human reasoner, while constructing provably safe concurrent code. We present several reasoning challenges involved in transforming the sequential data structure into its equivalent concurrent version. All the reasoning tasks are encoded in ASP and our reasoner can make sound judgments to transform sequential code into concurrent code. To the best of our knowledge, our work is the first one to use commonsense reasoning to automatically transform sequential programs into concurrent code. We also have developed a tool that we describe that relies on state-of-the-art ASP solvers and performs the reasoning tasks involved to generate concurrent code.
△ Less
Submitted 16 September, 2021;
originally announced September 2021.
-
Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming
Authors:
Brendan Hall,
Sarat Chandra Varanasi,
Jan Fiedor,
Joaquín Arias,
Kinjal Basu,
Fang Li,
Devesh Bhatt,
Kevin Driscoll,
Elmer Salazar,
Gopal Gupta
Abstract:
We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and…
▽ More
We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and change. We also show how answer set programming (ASP) and its query-driven implementation s(CASP) can be used to directly realize the event calculus model of the requirements. This event calculus model can be used to automatically validate the requirements. Since ASP is an expressive knowledge representation language, it can also be used to represent contextual knowledge about cyber-physical systems, which, in turn, can be used to find gaps in their requirements specifications. We illustrate our approach through an altitude alerting system from the avionics domain.
△ Less
Submitted 9 September, 2021;
originally announced September 2021.
-
Acoustical characteristics of segmented plates with contact interfaces
Authors:
Srinivas Varanasi,
Thomas Siegmund,
J. Stuart Bolton
Abstract:
The possibility of shifting sound energy from lower to higher frequency bands is investigated. The system configuration considered is a segmented structure having non-linear stiffness characteristics. It is proposed here that such a frequency-shifting mechanism could complement metamaterial concepts for mass-efficient sound barriers. The acoustical behavior of the material system was studied throu…
▽ More
The possibility of shifting sound energy from lower to higher frequency bands is investigated. The system configuration considered is a segmented structure having non-linear stiffness characteristics. It is proposed here that such a frequency-shifting mechanism could complement metamaterial concepts for mass-efficient sound barriers. The acoustical behavior of the material system was studied through a representative two-dimensional model consisting of a segmented plate with a contact interface. Multiple harmonic peaks were observed in response to a purely single frequency excitation, and the strength of the response was found to depend on the degree of non-linearity introduced. The lower and closer an excitation frequency was to the characteristic resonance frequencies of the base system, the stronger was the predicted higher harmonic response. The broadband sound transmission loss of these systems has also been calculated and the low frequency sound transmission loss was found to increase as the level of the broadband incident sound field increased. The present findings support the feasibility of designing material systems that transfer energy from lower frequency bands, where a sound barrier is less efficient, to higher bands where energy is more readily dissipated.
△ Less
Submitted 5 February, 2021;
originally announced February 2021.
-
Knowledge-driven Natural Language Understanding of English Text and its Applications
Authors:
Kinjal Basu,
Sarat Varanasi,
Farhad Shakerin,
Joaquin Arias,
Gopal Gupta
Abstract:
Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) research. An ideal NLU system should process a language in a way that is not exclusive to a single task or a dataset. Kee** this in mind, we have introduced a novel knowledge driven semantic representation approach for English text. By leveraging the VerbNet lexicon, we are able to map syntax t…
▽ More
Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) research. An ideal NLU system should process a language in a way that is not exclusive to a single task or a dataset. Kee** this in mind, we have introduced a novel knowledge driven semantic representation approach for English text. By leveraging the VerbNet lexicon, we are able to map syntax tree of the text to its commonsense meaning represented using basic knowledge primitives. The general purpose knowledge represented from our approach can be used to build any reasoning based NLU system that can also provide justification. We applied this approach to construct two NLU applications that we present here: SQuARE (Semantic-based Question Answering and Reasoning Engine) and StaCACK (Stateful Conversational Agent using Commonsense Knowledge). Both these systems work by "truly understanding" the natural language text they process and both provide natural language explanations for their responses while maintaining high accuracy.
△ Less
Submitted 27 January, 2021;
originally announced January 2021.
-
Generating Concurrent Programs From Sequential Data Structure Knowledge
Authors:
Sarat Chandra Varanasi,
Neeraj Mittal,
Gopal Gupta
Abstract:
In this paper we tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions.…
▽ More
In this paper we tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using automated commonsense reasoning. We assume that the data structure description is provided as axioms alongside the sequential code of its algebraic operations. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees. Knowledge in our case is expressed using Answer Set Programming (ASP), and we employ deduction, induction and abduction---just as humans do---in the reasoning involved. ASP allows for succinct modeling of first order theories of pointer data structures, run-time thread interactions and shared memory synchronization. Our reasoner can systematically make the same judgments as a human reasoner while constructing provably safe concurrent code. We present several reasoning challenges involved in transforming the sequential data structure into its equivalent concurrent version. All the reasoning tasks are encoded in ASP and our reasoner can make sound judgments to transform sequential code into concurrent code. To the best of our knowledge, our work is the first one to use commonsense reasoning to automatically transform sequential programs into concurrent code.
△ Less
Submitted 8 November, 2020;
originally announced November 2020.
-
Machine-learning-enhanced time-of-flight mass spectrometry analysis
Authors:
Ye Wei,
Rama Srinivas Varanasi,
Torsten Schwarz,
Leonie Gomell,
Huan Zhao,
David J. Larson,
Binhan Sun,
Geng Liu,
Hao Chen,
Dierk Raabe,
Baptiste Gault
Abstract:
Mass spectrometry is a widespread approach to work out what are the constituents of a material. Atoms and molecules are removed from the material and collected, and subsequently, a critical step is to infer their correct identities based from patterns formed in their mass-to-charge ratios and relative isotopic abundances. However, this identification step still mainly relies on individual user's e…
▽ More
Mass spectrometry is a widespread approach to work out what are the constituents of a material. Atoms and molecules are removed from the material and collected, and subsequently, a critical step is to infer their correct identities based from patterns formed in their mass-to-charge ratios and relative isotopic abundances. However, this identification step still mainly relies on individual user's expertise, making its standardization challenging, and hindering efficient data processing. Here, we introduce an approach that leverages modern machine learning technique to identify peak patterns in time-of-flight mass spectra within microseconds, outperforming human users without loss of accuracy. Our approach is cross-validated on mass spectra generated from different time-of-flight mass spectrometry(ToF-MS) techniques, offering the ToF-MS community an open-source, intelligent mass spectra analysis.
△ Less
Submitted 2 October, 2020;
originally announced October 2020.
-
SQuARE: Semantics-based Question Answering and Reasoning Engine
Authors:
Kinjal Basu,
Sarat Chandra Varanasi,
Farhad Shakerin,
Gopal Gupta
Abstract:
Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) and from its early days, it has received significant attention through question answering (QA) tasks. We introduce a general semantics-based framework for natural language QA and also describe the SQuARE system, an application of this framework. The framework is based on the denotational semantic…
▽ More
Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) and from its early days, it has received significant attention through question answering (QA) tasks. We introduce a general semantics-based framework for natural language QA and also describe the SQuARE system, an application of this framework. The framework is based on the denotational semantics approach widely used in programming language research. In our framework, valuation function maps syntax tree of the text to its commonsense meaning represented using basic knowledge primitives (the semantic algebra) coded using answer set programming (ASP). We illustrate an application of this framework by using VerbNet primitives as our semantic algebra and a novel algorithm based on partial tree matching that generates an answer set program that represents the knowledge in the text. A question posed against that text is converted into an ASP query using the same framework and executed using the s(CASP) goal-directed ASP system. Our approach is based purely on (commonsense) reasoning. SQuARE achieves 100% accuracy on all the five datasets of bAbI QA tasks that we have tested. The significance of our work is that, unlike other machine learning based approaches, ours is based on "understanding" the text and does not require any training. SQuARE can also generate an explanation for an answer while maintaining high accuracy.
△ Less
Submitted 21 September, 2020;
originally announced September 2020.
-
LowFER: Low-rank Bilinear Pooling for Link Prediction
Authors:
Saadullah Amin,
Stalin Varanasi,
Katherine Ann Dunfield,
Günter Neumann
Abstract:
Knowledge graphs are incomplete by nature, with only a limited number of observed facts from the world knowledge being represented as structured relations between entities. To partly address this issue, an important task in statistical relational learning is that of link prediction or knowledge graph completion. Both linear and non-linear models have been proposed to solve the problem. Bilinear mo…
▽ More
Knowledge graphs are incomplete by nature, with only a limited number of observed facts from the world knowledge being represented as structured relations between entities. To partly address this issue, an important task in statistical relational learning is that of link prediction or knowledge graph completion. Both linear and non-linear models have been proposed to solve the problem. Bilinear models, while expressive, are prone to overfitting and lead to quadratic growth of parameters in number of relations. Simpler models have become more standard, with certain constraints on bilinear map as relation parameters. In this work, we propose a factorized bilinear pooling model, commonly used in multi-modal learning, for better fusion of entities and relations, leading to an efficient and constraint-free model. We prove that our model is fully expressive, providing bounds on the embedding dimensionality and factorization rank. Our model naturally generalizes Tucker decomposition based TuckER model, which has been shown to generalize other models, as efficient low-rank approximation without substantially compromising the performance. Due to low-rank approximation, the model complexity can be controlled by the factorization rank, avoiding the possible cubic growth of TuckER. Empirically, we evaluate on real-world datasets, reaching on par or state-of-the-art performance. At extreme low-ranks, model preserves the performance while staying parameter efficient.
△ Less
Submitted 25 August, 2020;
originally announced August 2020.
-
Pointer Data Structure Synthesis from Answer Set Programming Specifications
Authors:
Sarat Chandra Varanasi,
Neeraj Mittal,
Gopal Gupta
Abstract:
We develop an inductive proof-technique to generate imperative programs for pointer data structures from behavioural specifications expressed in the Answer Set Programming (ASP) formalism. ASP is a non-monotonic logic based formalism that employs negation-as-failure which helps emulate the human thought process, allowing domain experts to model desired system behaviour succinctly. We argue in this…
▽ More
We develop an inductive proof-technique to generate imperative programs for pointer data structures from behavioural specifications expressed in the Answer Set Programming (ASP) formalism. ASP is a non-monotonic logic based formalism that employs negation-as-failure which helps emulate the human thought process, allowing domain experts to model desired system behaviour succinctly. We argue in this paper that ASP's reliance on negation-as-failure makes it a better formalism than those based on first-order logic for writing formal specifications. We assume the a domain expert provides the representation of inductively defined data structures along with a specification of its operations. Our procedures combined with our novel proof-technique reason over the specifications and automatically generate an imperative program. Our proof-technique leverages the idea of partial deduction to simplify logical specifications. By algebraically simplifying logical specifications we arrive at a residual specification which can be interpreted as an appropriate imperative program. This work is in the realm of constructing programs that are correct according to a given specification.
△ Less
Submitted 12 August, 2020; v1 submitted 12 June, 2020;
originally announced June 2020.
-
Imperative Program Synthesis from Answer Set Programs
Authors:
Sarat Chandra Varanasi
Abstract:
Our research concerns generating imperative programs from Answer Set Programming Specifications. ASP is highly declarative and is ideal for writing specifications. Further with negation-as-failure it is easy to succinctly represent combinatorial search problems. We are currently working on synthesizing imperative programs from ASP programs by turning the negation into useful computations. This ope…
▽ More
Our research concerns generating imperative programs from Answer Set Programming Specifications. ASP is highly declarative and is ideal for writing specifications. Further with negation-as-failure it is easy to succinctly represent combinatorial search problems. We are currently working on synthesizing imperative programs from ASP programs by turning the negation into useful computations. This opens up a novel way to synthesize programs from executable specifications.
△ Less
Submitted 19 September, 2019;
originally announced September 2019.
