Dept. of Computer Science
http://hdl.handle.net/2142/10755
Sun, 25 Feb 2018 12:00:10 GMT2018-02-25T12:00:10ZComplexity analysis of distributed operator placement and resource provisioning for IoT applications
http://hdl.handle.net/2142/99062
Complexity analysis of distributed operator placement and resource provisioning for IoT applications
Sandur Atul; Elgamal Tarek; Agha Gul; Nahrstedt Klara
Internet of Things (IoT) applications generate massive amounts of real-time data. Owners of such data strive to make predictions/inference from large streams of complex input such as video feeds, often by deploying applications that involve machine learning and image processing operations. A typical deployment of IoT applications includes edge devices to acquire the input data and provide processing/storage capacity closer to the location where the data is captured. An important challenge for IoT applications is deciding which operations to be executed on an edge device and which operations should be carried out on the cloud. In this report, we present computational complexity analysis of a dynamic programming algorithm called Droplet, to scalably partition operations in IoT applications across shared edge and cloud resources, while jointly minimizing the completion time of all operations and resource consumption.
We analyze Droplet to show it scales linearly in the total number of operations.
complexity, placement, distributed, edge devices, cloud, DAG
Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/2142/990622018-01-01T00:00:00ZSandur AtulElgamal TarekAgha GulNahrstedt KlaraFormal Modeling and Analysis of Mobile Ad hoc Networks in Real-Time Maude
http://hdl.handle.net/2142/99047
Formal Modeling and Analysis of Mobile Ad hoc Networks in Real-Time Maude
Liu, Si; Olveczky, Peter C.; Meseguer, Jose
Modeling and analyzing Mobile Ad-hoc Networks (MANETs) pose
non-trivial challenges to formal methods. Time, geometry,
communication delays and failures, mobility, and uni- and
bidirectional wireless communication can interact in unforeseen ways
that are hard to model and analyze by current process calculi and
automatic formal methods. As a consequence, current analyses tend
to abstract away these physical aspects, so that---although still
quite useful in finding various errors---their simplifying
assumptions can easily fail to model details of MANET behavior
relevant to meet desired requirements.
In this work we present a formal framework for the
modeling and analysis of MANETS based on Real-Time Maude to address
this challenge. Specifically, we show that our framework has good
expressive power to model relevant aspects of MANETs, and good
compositionality properties, so that a MANET protocol can be easily
composed with various models of mobility and with other MANET protocols.
We illustrate the use of our framework on two well-known MANET
benchmarks: the AODV routing protocol and the leader election protocol
of Vasudevan, Kurose, and Towsley. Our formal analysis has
uncovered a spurious behavior in the latter protocol that
is due to the subtle interplay between communication delays, node movement, and
neighbor discovery. This behavior therefore cannot be found by
analyses that abstract from node movement and communication delays.
Mobile Ad-hoc Networks; Formal Specification; Model Checking; Real-Time Maude
Fri, 01 Jan 2016 00:00:00 GMThttp://hdl.handle.net/2142/990472016-01-01T00:00:00ZLiu, SiOlveczky, Peter C.Meseguer, JoseA New Distributed Transaction Protocol and Its Formal Analysis in Maude
http://hdl.handle.net/2142/99046
A New Distributed Transaction Protocol and Its Formal Analysis in Maude
Liu, Si; Olveczky, Peter C.; Santhanam, Keshav; Wang, Qi; Gupta, Indranil; Meseguer, Jose
Designers of distributed database systems face the choice between performance and consistency guarantees: with stronger consistency guarantees comes higher transactional latency and lower throughput. Certain collaborative editing application scenarios only require read atomicity (either all or none of a transaction's updates are visible to another transaction) and no lost updates (all updates are incrementally performed). Many existing distributed database systems meet these requirements. However, they all provide additional stronger
consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets application scenarios where only read atomicity and no lost updates are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA's satisfaction of read atomicity and prevention of lost updates. Our results show that ROLA satisfies the correctness properties with a bounded number of parameters. To analyze performance we: (a) perform statistical model checking to analyze key performance properties such as throughput, averange latency, and commit rate; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the same performance properties for Walter, a well-known high-performance protocol meeting the requirements of read atomicity and preservation of lost updates. Our statistical model checking results show that ROLA outperforms Walter.
Statistical Model Checking; Performance; Maude; Rewriting Logic; Distributed Database System; Transaction Protocol; Consistency Model
Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/2142/990462018-01-01T00:00:00ZLiu, SiOlveczky, Peter C.Santhanam, KeshavWang, QiGupta, IndranilMeseguer, JoseVariant Satisfiability in Initial Algebras with Predicates
http://hdl.handle.net/2142/99039
Variant Satisfiability in Initial Algebras with Predicates
Gutierrez Raul; Meseguer Jose
Decision procedures can be either theory-specific,
e.g., Presburger arithmetic, or theory-generic, applying to
an infinite number of user-definable theories. Variant
satisfiability is a theory-generic procedure for quantifier-free
satisfiability in the initial algebra of an order-sorted equational theory
(Sigma,E U B) under two conditions: (i) E U B has the
finite variant property and B has a finitary unification
algorithm; and (ii) (Sigma,E U B) protects a constructor
subtheory (Omega,E_{Omega} U B_{Omega}) that is
OS-compact. These conditions apply to many
user-definable theories, but have a main limitation: they apply well to
data structures, but often do not hold for
user-definable predicates on such data structures.
We present a theory-generic satisfiability decision
procedure, and a prototype implementation, extending variant-based
satisfiability to initial algebras with user-definable predicates under
fairly general conditions.
finite variant property (FVP); OS-compactness; user-definable predicates; decidable validity and satisfiability in initial algebras
Mon, 12 Feb 2018 00:00:00 GMThttp://hdl.handle.net/2142/990392018-02-12T00:00:00ZGutierrez RaulMeseguer JoseFormal Modeling and Analysis of the Walter Transactional Data Store
http://hdl.handle.net/2142/98988
Formal Modeling and Analysis of the Walter Transactional Data Store
Liu, Si; Olveczky, Peter C.; Wang, Qi; Meseguer, Jose
Walter is a distributed partially replicated data store
providing Parallel Snapshot Isolation (PSI), an important consistency property that offers attractive performance while ensuring adequate guarantees for certain kinds of applications.
In this work we formally model Walter's design in Maude and formally specify and verify PSI by model checking. To also analyze Walter's performance we extend the Maude specification of Walter to a probabilistic rewrite theory and perform statistical model checking analysis to evaluate Walter's throughput for a wide range of workloads. Our performance results are consistent
with a previous experimental evaluation and throw new light on
Walter's performance for different workloads not evaluated before.
Maude; Model Checking; Statistical Model Checking; Parallel Snapshot Isolation; Transactional Data Store; Performance
Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/2142/989882018-01-01T00:00:00ZLiu, SiOlveczky, Peter C.Wang, QiMeseguer, JoseLearning viewer-centered projections for 3D shape completion
http://hdl.handle.net/2142/98435
Learning viewer-centered projections for 3D shape completion
Shin, Daeyun
The goal of this study is to determine the effectiveness of different 3D shape representations in learning to generate volumetric shapes using deep neural networks. We propose to automatically reconstruct a 3D model from a single-view image of an object by synthesizing multiple depth images and inferring the volume through multi-view 3D reconstruction. The final output is a 3D mesh inferred without seeing voxels in the training process. This is similar to the intuition that humans remember (and inherently reproduce) 3D shapes without ever "seeing through" the underlying volume – we think of objects as seen from certain viewpoints and 3D structure is a derived concept. Most previous studies have focused on directly learning the voxel representations, deforming exemplars, or utilizing user interaction. In this paper, we want to learn category-independent object shape representations by simultaneously predicting multiple incomplete surfaces in relation to the viewer with the complete 3D structure in mind. Instead of predicting voxels which typically need to be in low resolution, we hypothesize that learning a representation that can consistently produce partial surfaces in a multi-task learning model enables inter-category 3D shape transfer. We perform shape completion in novel categories and evaluate quantitatively using voxel I/U and surface distance metrics. We also report that the learned representation improves 3D shape classification.
3D shape learning; Deep encoder-decoder networks; Vision for graphics; Multi-view reconstruction
Thu, 20 Jul 2017 00:00:00 GMThttp://hdl.handle.net/2142/984352017-07-20T00:00:00ZShin, DaeyunApproximation algorithms for the minimum congestion routing problem via k-route flows
http://hdl.handle.net/2142/98428
Approximation algorithms for the minimum congestion routing problem via k-route flows
Idleman, Mark
Given a directed network G = (V,E) with source and target nodes s and t, respectively, and an integral capacity c_e on each edge e in E, an elementary k-flow is defined as a flow of 1 unit along each of k edge-disjoint s-t paths. A k-route flow, first introduced as a concept by Kishimoto, is defined as a non-negative linear sum of elementary k-flows. In this thesis, the study of k-route flows is extended by presenting efficient algorithms to calculate exact and approximate decompositions of k-route flows into their constituent elementary k-flows.
In addition, such decomposition algorithms are shown to prove useful in developing approximation algorithms for the well-studied Minimum Congestion Routing Problem. Given a directed network G = (V,E), a set of source-sink pairs {(s_1, t_1), ..., (s_l, t_l)}, and an integer k, the goal of the Minimum Congestion Routing Problem is to find k edge-disjoint paths between each pair (s_i, t_i) while minimizing the congestion over all chosen paths (defined as the maximum over all edges of the number of chosen paths that share a single edge). Early applications of randomized rounding introduced by Raghavan and Tompson provided a simple approximation algorithm for the case where k=1, but attempts to achieve similar approximation bounds in the case where k>1 have up until this point required the use of more advanced dependent rounding schemes. Utilizing the k-route flow decomposition algorithms presented in this thesis, we propose approximation algorithms for the Minimum Congestion Routing Problem for the case where k>1 that mimic the straightforward approach of Raghavan and Tompson while achieving identical approximation guarantees. Finally, we implement two variants of the exact k-route flow decomposition algorithm proposed in this thesis, and experimentally compare their performance using flows generated from various graph structures.
Minimum congestion routing; K-route flow; Network flow; Flow; Decomposition
Wed, 19 Jul 2017 00:00:00 GMThttp://hdl.handle.net/2142/984282017-07-19T00:00:00ZIdleman, MarkStudy of router software performance
http://hdl.handle.net/2142/98407
Study of router software performance
Chen, Yongli
Understanding router software performance is crucial for organizations which demand the optimal network quality. Because processing capability has heavy inﬂuence to communication networks [1], we need a benchmark for network administrators to choose the routers with the best performance per demand. However, it is hard to ﬁnd such benchmark at present. In this work, we study router software performance, which is a dominant factor for both control and management plane performances. We ﬁrstly introduce Packet Generator and a framework for network professionals to measure and understand router control plane performance. The Packet Generator is capable of sending and receiving network traﬃc with highest degrees of freedom, which enables users to test router control plane performance under various scenarios, ranging from a single device to a complex network topology. Then we conduct management plane experiments against various network topologies and router software versions.
Computer networks; Computer networking; Router; Control plane; Management plane; Performance; Border Gateway Protocol (BGP); Protocol Independent Multicast Sparse Mode (PIM-SM); Internet Group Management Protocol Version 3 (IGMPv3)
Mon, 17 Jul 2017 00:00:00 GMThttp://hdl.handle.net/2142/984072017-07-17T00:00:00ZChen, YongliOn lexical level matching
http://hdl.handle.net/2142/98404
On lexical level matching
Ling, Shaoshi
In many natural language understanding applications, text processing requires comparing lexical units: words, phrases, name entities and sentences. A significant amount of research has taken place in studying evaluating similarity metrics between those units. In this thesis, we summarize some research work in computing lexical similarity. We describe a new approach to compute similarity between two spans of text, using multiple semantic-units level comparison measures to compute sentence-level similarity scores.
Natural language processing (NLP); Similarity
Mon, 17 Jul 2017 00:00:00 GMThttp://hdl.handle.net/2142/984042017-07-17T00:00:00ZLing, ShaoshiSome results on symmetric signings
http://hdl.handle.net/2142/98401
Some results on symmetric signings
Carlson, Charles A
In this work, we investigate several natural computational problems related to identifying symmetric signings of symmetric matrices with specific spectral properties. We show NP-completeness for verifying whether an arbitrary matrix has a symmetric signing that is positive semi-definite, is singular, or has bounded eigenvalues. We exhibit a stark contrast between invertibility and the above-mentioned spectral properties by presenting a combinatorial characterization of matrices with invertible symmetric signings and an efficient algorithm using this characterization to verify whether a given matrix has an invertible symmetric signing. Finally, we give efficient algorithms to verify and find invertible and singular symmetric signing for matrices whose support graph is bipartite.
Matrix signings; Spectral graph theory; Eigenvalues; Matchings; Determinant
Mon, 17 Jul 2017 00:00:00 GMThttp://hdl.handle.net/2142/984012017-07-17T00:00:00ZCarlson, Charles A