etd@IISc Collection:
http://etd.iisc.ernet.in/2005/18
Fri, 22 Jun 2018 00:05:08 GMT2018-06-22T00:05:08ZNumber Theoretic, Computational and Cryptographic Aspects of a Certain Sequence of Arithmetic Progressions
http://etd.iisc.ernet.in/2005/3741
Title: Number Theoretic, Computational and Cryptographic Aspects of a Certain Sequence of Arithmetic Progressions
Authors: Srikanth, Cherukupally
Abstract: This thesis introduces a new mathematical object: collection of arithmetic progressions with elements satisfying the inverse property, \j-th terms of i-th and (i+1)-th progressions are multiplicative inverses of each other modulo (j+1)-th term of i-th progression".
Such a collection is uniquely de ned for any pair (a; d) of co-prime integers. The progressions of the collection are ordered. Thus we call it a sequence rather than a collection. The results of the thesis are on the following number theoretic, computational and cryptographic aspects of the defined sequence and its generalizations.
The sequence is closely connected to the classical Euclidean algorithm. Precisely, certain consecutive progressions of the sequence form \groupings". The difference between the common differences of any two consecutive progressions of a grouping is same. The number of progressions in a grouping is connected to the quotient sequence of the Euclidean algorithm on co-prime input pairs. The research community has studied extensively the behavior of the Euclidean algorithm. For the rst time in the literature, the connection (proven in the thesis) shows what the quotients of the algorithm signify. Further, the leading terms of progressions within groupings satisfy a mirror image symmetry property, called \symmetricity". The property is subject to the quotient sequence of the Euclidean algorithm and divisors of integers of the form x2 y2 falling in specific intervals.
The integers a, d are the primary quantities of the defined sequence in a computational sense. Given the two, leading term and common difference of any progression of the sequence can be computed in time quadratic in the binary length of d. On the other hand, the inverse computational question of finding (a; d), given information on some terms of the sequence, is interesting. This problem turns out to be hard as it requires finding solutions to an nearly-determined system of multivariate polynomial equations. Two sub-problems arising in this context are shown to be equivalent to the problem of factoring integers. The reduction to the factoring problem, in both cases, is probabilistic.
Utilizing the computational difficulty of solving the inverse problem, and the sub-problems (mentioned above), we propose a symmetric-key cryptographic scheme (SKCS), and a public key cryptographic scheme (PKCS). The PKCS is also based on the hardness of the problem of finding square-roots modulo composite integers. Our proposal uses the same algorithmic and computational primitives for effecting both the PKCS and SKCS. In addition, we use the notion of the sequence of arithmetic progressions to design an entity authentication scheme.
The proof of equivalence between one of the inverse computational problems (mentioned above) and integer factoring led us to formulate and investigate an independent problem concerning the largest divisor of integer N bounded by the square-root of N. We present some algorithmic and combinatorial results.
In the course of the above investigations, we are led to certain open questions of number theoretic, combinatorial and algorithmic nature. These pertain to the quotient sequence of the Euclidean algorithm, divisors of integers of the form x2 y2 p in specific intervals, and the largest divisor of integer N bounded by N.Wed, 20 Jun 2018 18:30:00 GMThttp://etd.iisc.ernet.in/2005/37412018-06-20T18:30:00ZA Refinement-Based Methodology for Verifying Abstract Data Type Implementations
http://etd.iisc.ernet.in/2005/3744
Title: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations
Authors: Divakaran, Sumesh
Abstract: This thesis is about techniques for proving the functional correctness of Abstract Data Type (ADT) implementations. We provide a framework for proving the functional correctness of imperative language implementations of ADTs, using a theory of refinement. We develop a theory of refinement to reason about both declarative and imperative language implementations of ADTs. Our theory facilitates compositional reasoning about complex implementations that may use several layers of sub-ADTs.
Based on our theory of refinement, we propose a methodology for proving the functional correctness of an existing imperative language implementation of an ADT. We propose a mechanizable translation from an abstract model in the Z language to an abstract implementation in VCC’s ghost language. Then we present a technique to carry out the refinement checks completely within the VCC tool.
We apply our proposed methodology to prove the functional correctness of the scheduling-related functionality of FreeRTOS, a popular open-source real-time operating system. We focused on the scheduler-related functionality, found major deviations from the intended behavior, and did a machine-checked proof of the correctness of the fixed code.
We also present an eﬃcient way to phrase the refinement conditions in VCC, which considerably improves VCC’s performance. We evaluated this technique on a simplified version of FreeRTOS which we constructed for this verification exercise. Using our eﬃcient approach, VCC always terminates and leads to a reduction of over 90% in the total time taken by a naive check, when evaluated on this case-study.Wed, 20 Jun 2018 18:30:00 GMThttp://etd.iisc.ernet.in/2005/37442018-06-20T18:30:00ZMulti-label Classification with Multiple Label Correlation Orders And Structures
http://etd.iisc.ernet.in/2005/3719
Title: Multi-label Classification with Multiple Label Correlation Orders And Structures
Authors: Posinasetty, Anusha
Abstract: Multilabel classification has attracted much interest in recent times due to the wide applicability of the problem and the challenges involved in learning a classifier for multilabeled data. A crucial aspect of multilabel classification is to discover the structure and order of correlations among labels and their effect on the quality of the classifier. In this work, we propose a structural Support Vector Machine (structural SVM) based framework which enables us to systematically investigate the importance of label correlations in multi-label classification. The proposed framework is very flexible and provides a unified approach to handle multiple correlation orders and structures in an adaptive manner and helps to effectively assess the importance of label correlations in improving the generalization performance. We perform extensive empirical evaluation on several datasets from different domains and present results on various performance metrics. Our experiments provide for the first time, interesting insights into the following questions: a) Are label correlations always beneficial in multilabel classification? b) What effect do label correlations have on multiple performance metrics typically used in multilabel classification? c) Is label correlation order significant and if so, what would be the favorable correlation order for a given dataset and a given performance metric? and d) Can we make useful suggestions on the label correlation structure?Sun, 17 Jun 2018 18:30:00 GMThttp://etd.iisc.ernet.in/2005/37192018-06-17T18:30:00ZAutomatic Optimization of Geometric Multigrid Methods using a DSL Approach
http://etd.iisc.ernet.in/2005/3707
Title: Automatic Optimization of Geometric Multigrid Methods using a DSL Approach
Authors: Vasista, Vinay V
Abstract: Geometric Multigrid (GMG) methods are widely used in numerical analysis to accelerate the convergence of partial differential equations solvers using a hierarchy of grid discretizations. These solvers find plenty of applications in various fields in engineering and scientific domains, where solving PDEs is of fundamental importance. Using multigrid methods, the pace at which the solvers arrive at the solution can be improved at an algorithmic level. With the advance in modern computer architecture, solving problems with higher complexity and sizes is feasible - this is also the case with multigrid methods. However, since hardware support alone cannot achieve high performance in execution time, there is a need for good software that help programmers in doing so.
Multiple grid sizes and recursive expression of multigrid cycles make the task of manual program optimization tedious and error-prone. A high-level language that aids domain experts to quickly express complex algorithms in a compact way using dedicated constructs for multigrid methods and with good optimization support is thus valuable. Typical computation patterns in a GMG algorithm includes stencils, point-wise accesses, restriction and interpolation of a grid. These computations can be optimized for performance on modern architectures using standard parallelization and locality enhancement techniques.
Several past works have addressed the problem of automatic optimizations of computations in various scientific domains using a domain-specific language (DSL) approach. A DSL is a language with features to express domain-specific computations and compiler support to enable optimizations specific to these computations. Halide and PolyMage are two of the recent works in this direction, that aim to optimize image processing pipelines. Many computations like upsampling and downsampling an image are similar to interpolation and restriction in geometric multigrid methods.
In this thesis, we demonstrate how high performance can be achieved on GMG algorithms written in the PolyMage domain-specific language with new optimizations we added to the compiler. We also discuss the implementation of non-trivial optimizations, on PolyMage compiler, necessary to achieve high parallel performance for multigrid methods on modern architectures. We realize these goals by:
• introducing multigrid domain-specific constructs to minimize the verbosity of the algorithm specification;
• storage remapping to reduce the memory footprint of the program and improve cache locality exploitation;
• mitigating execution time spent in data handling operations like memory allocation and freeing, using a pool of memory, across multiple multigrid cycles; and
• incorporating other well-known techniques to leverage performance, like exploiting multi-dimensional parallelism and minimizing the lifetime of storage buffers.
We evaluate our optimizations on a modern multicore system using five different benchmarks varying in multigrid cycle structure, complexity and size, for two-and three-dimensional data grids. Experimental results show that our optimizations:
• improve performance of existing PolyMage optimizer by 1.31x;
• are better than straight-forward parallel and vector implementations by 3.2x;
• are better than hand-optimized versions in conjunction with optimizations by Pluto, a state-of-the-art polyhedral source-to-source optimizer, by 1.23x; and
• achieve up to 1.5$\times$ speedup over NAS MG benchmark from the NAS Parallel Benchmarks.
(The speedup numbers are Geometric means over all benchmarks)Wed, 13 Jun 2018 18:30:00 GMThttp://etd.iisc.ernet.in/2005/37072018-06-13T18:30:00Z