Showing 1–10 of 10 results for author: Tunc, C

Optimal Digital Twinning of Random Systems with Twinning Rate Constraints

Authors: Caglar Tunc

Abstract: With the massive advancements in processing power, Digital Twins (DTs) have become powerful tools to monitor and analyze physical entities. However, due to the potentially very high number of Physical Systems (PSs) to be tracked and emulated, for instance, in a factory environment or an Internet of Things (IoT) network, continuous twinning might become infeasible. In this paper, a DT system is inv… ▽ More With the massive advancements in processing power, Digital Twins (DTs) have become powerful tools to monitor and analyze physical entities. However, due to the potentially very high number of Physical Systems (PSs) to be tracked and emulated, for instance, in a factory environment or an Internet of Things (IoT) network, continuous twinning might become infeasible. In this paper, a DT system is investigated with a set of random PSs, where the twinning rate is limited due to resource constraints. Three cost functions are considered to quantify and penalize the twinning delay. For these cost functions, the optimal twinning problem under twinning rate constraints is formulated. In a numerical example, the proposed cost functions are evaluated for two, one push-based and one pull-based, benchmark twinning policies. The proposed methodology is the first to investigate the optimal twinning problem with random PSs and twinning rate constraints, and serves as a guideline for real-world implementations on how frequently PSs should be twinned. △ Less

Submitted 3 October, 2024; originally announced October 2024.

DTRAN: A Special Use Case of RAN Optimization using Digital Twin

Authors: Caglar Tunc, Kubra Duran, Buse Bilgin, Gokhan Kalem, Berk Canberk

Abstract: The emergence of beyond 5G (B5G) and 6G networks underscores the critical role of advanced computer-aided tools, such as network digital twins (DTs), in fostering autonomous networks and ubiquitous intelligence. Existing solutions in the DT domain primarily aim to model and automate specific tasks within the network lifecycle, which lack flexibility and adaptability for fully autonomous design and… ▽ More The emergence of beyond 5G (B5G) and 6G networks underscores the critical role of advanced computer-aided tools, such as network digital twins (DTs), in fostering autonomous networks and ubiquitous intelligence. Existing solutions in the DT domain primarily aim to model and automate specific tasks within the network lifecycle, which lack flexibility and adaptability for fully autonomous design and management. Unlike the existing DT approaches, we propose RAN optimization using the Digital Twin (DTRAN) framework that follows a holistic approach from core to edge networks. The proposed DTRAN framework enables real-time data management and communication with the physical network, which provides a more accurate and detailed digital replica than the existing approaches. We outline the main building blocks of the DTRAN and describe the details of our specific use case, which is RAN configuration optimization, to demonstrate the applicability of the proposed framework for a real-world scenario. △ Less

Submitted 2 September, 2024; originally announced September 2024.

CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution Analysis

Authors: Hünkar Can Tunç, Ameya Prashant Deshmukh, Berk Çirisci, Constantin Enea, Andreas Pavlogiannis

Abstract: Dynamic analyses are a standard approach to analyzing and testing concurrent programs. Such techniques observe program traces and analyze them to infer the presence or absence of bugs. At its core, each analysis maintains a partial order $P$ that represents order dependencies between events of the analyzed trace $σ$. Naturally, the scalability of the analysis largely depends on how efficiently it… ▽ More Dynamic analyses are a standard approach to analyzing and testing concurrent programs. Such techniques observe program traces and analyze them to infer the presence or absence of bugs. At its core, each analysis maintains a partial order $P$ that represents order dependencies between events of the analyzed trace $σ$. Naturally, the scalability of the analysis largely depends on how efficiently it maintains $P$. The standard data structure for this task has thus far been vector clocks. These, however, are slow for analyses that follow a non-streaming style, costing $O(n)$ for inserting (and propagating) each new ordering in $P$, where $n$ is the size of $σ$, while they cannot handle the deletion of existing orderings. In this paper we develop collective sparse segment trees (CSSTs), a simple but elegant data structure for generically maintaining a partial order $P$. CSSTs thrive when the width $k$ of $P$ is much smaller than the size $n$ of its domain, allowing inserting, deleting, and querying for orderings in $P$ to run in $O(logn)$ time. For a concurrent trace, $k$ is bounded by the number of its threads, and is normally orders of magnitude smaller than its size $n$, making CSSTs fitting for this setting. Our experimental results confirm that CSSTs are the best data structure currently to handle a range of dynamic analyses from existing literature. △ Less

Submitted 29 March, 2024; v1 submitted 26 March, 2024; originally announced March 2024.

Optimal Reads-From Consistency Checking for C11-Style Memory Models

Authors: Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, Andreas Pavlogiannis

Abstract: Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++.One of the most fundamental problems associated with a memory model M is consistency checking: given an execution X, is X consistent with M? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic anal… ▽ More Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++.One of the most fundamental problems associated with a memory model M is consistency checking: given an execution X, is X consistent with M? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic analyses. As such, it has been explored extensively and its complexity is well-understood for traditional models like SC and TSO. However, less is known for the numerous model variants of C/C++, for which the problem becomes challenging due to the intricacies of their concurrency primitives. In this work we study the problem of consistency checking for popular variants of the C11 memory model, in particular, the RC20 model, its release-acquire (RA) fragment, the strong and weak variants of RA (SRA and WRA), as well as the Relaxed fragment of RC20. Motivated by applications in testing and model checking, we focus on reads-from consistency checking. The input is an execution X specifying a set of events, their program order and their reads-from relation, and the task is to decide the existence of a modification order on the writes of X that makes X consistent in a memory model. We draw a rich complexity landscape for this problem; our results include (i)~nearly-linear-time algorithms for certain variants, which improve over prior results, (ii)~fine-grained optimality results, as well as (iii)~matching upper and lower bounds (NP-hardness) for other variants. To our knowledge, this is the first work to characterize the complexity of consistency checking for C11 memory models. We have implemented our algorithms inside the TruSt model checker and the C11Tester testing tool. Experiments on standard benchmarks show that our new algorithms improve consistency checking, often by a significant margin. △ Less

Submitted 11 May, 2023; v1 submitted 7 April, 2023; originally announced April 2023.

Sound Dynamic Deadlock Prediction in Linear Time

Authors: Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

Abstract: Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detectio… ▽ More Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detection, such as data races. Effective dynamic deadlock prediction, however, has proven a challenging task, as no deadlock predictor currently meets the requirements of soundness, high-precision, and efficiency. In this paper, we first formally establish that this tradeoff is unavoidable, by showing that (a) sound and complete deadlock prediction is intractable, in general, and (b) even the seemingly simpler task of determining the presence of potential deadlocks, which often serve as unsound witnesses for actual predictable deadlocks, is intractable. The main contribution of this work is a new class of predictable deadlocks, called sync(hronization)-preserving deadlocks. Informally, these are deadlocks that can be predicted by reordering the observed execution while preserving the relative order of conflicting critical sections. We present two algorithms for sound deadlock prediction based on this notion. Our first algorithm SPDOffline detects all sync-preserving deadlocks, with running time that is linear per abstract deadlock pattern, a novel notion also introduced in this work. Our second algorithm SPDOnline predicts all sync-preserving deadlocks that involve two threads in a strictly online fashion, runs in overall linear time, and is better suited for a runtime monitoring setting. We implemented both our algorithms and evaluated their ability to perform offline and online deadlock-prediction on a large dataset of standard benchmarks. △ Less

Submitted 25 June, 2023; v1 submitted 7 April, 2023; originally announced April 2023.

A Tree Clock Data Structure for Causal Orderings in Concurrent Executions

Authors: Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, Mahesh Viswanathan

Abstract: Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a single program execution. Often a crucial step in these techniques is to define a causal ordering between events in the execution, which is then computed using vector clocks, a simple data structure that stores logical… ▽ More Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a single program execution. Often a crucial step in these techniques is to define a causal ordering between events in the execution, which is then computed using vector clocks, a simple data structure that stores logical times of threads. The two basic operations of vector clocks, namely join and copy, require $Θ(k)$ time, where $k$ is the number of threads. Thus they are a computational bottleneck when $k$ is large. In this work, we introduce tree clocks, a new data structure that replaces vector clocks for computing causal orderings in program executions. Joining and copying tree clocks takes time that is roughly proportional to the number of entries being modified, and hence the two operations do not suffer the a-priori $Θ(k)$ cost per application. We show that when used to compute the classic happens-before (HB) partial order, tree clocks are optimal, in the sense that no other data structure can lead to smaller asymptotic running time. Moreover, we demonstrate that tree clocks can be used to compute other partial orders, such as schedulable-happens-before (SHB) and the standard Mazurkiewicz (MAZ) partial order, and thus are a versatile data structure. Our experiments show that just by replacing vector clocks with tree clocks, the computation becomes from $2.02 \times$ faster (MAZ) to $2.66 \times$ (SHB) and $2.97 \times$ (HB) on average per benchmark. These results illustrate that tree clocks have the potential to become a standard data structure with wide applications in concurrent analyses. △ Less

Submitted 17 January, 2022; originally announced January 2022.

Explaining Safety Failures in NetKAT

Authors: Georgiana Caltais, Hunkar Can Tunc

Abstract: This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language based on a well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT). Amongst others, the mathematical foundation of NetKAT gave rise to a sound and complete equational theory.… ▽ More This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language based on a well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT). Amongst others, the mathematical foundation of NetKAT gave rise to a sound and complete equational theory. In our setting, a safe behaviour is characterised by a NetKAT policy, or program, which does not enable forwarding packets from an ingress i to an undesirable egress e. We show how explanations for safety violations can be derived in an equational fashion, according to a modification of the existing NetKAT axiomatisation. We propose an approach based on the Maude system for actually computing the undesired behaviours witnessing the forwarding of packets from i to e as above. SDN-SafeCheck is a tool based on Maude equational theories satisfying important properties such as Church-Rosser and termination. SDN-SafeCheck automatically identifies all the undesired behaviours leading to e, covering forwarding paths up to a user specified size. △ Less

Submitted 24 February, 2021; originally announced February 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:1909.01745

DyNetKAT: An Algebra of Dynamic Networks

Authors: Georgiana Caltais, Hossein Hojjat, Mohammad Mousavi, Hunkar Can Tunc

Abstract: We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the eq… ▽ More We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory to provide an efficient reasoning method about safety properties for dynamic networks. We implement our equational theory in DyNetiKAT -- a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our initial tool prototype. △ Less

Submitted 22 May, 2021; v1 submitted 19 February, 2021; originally announced February 2021.

Video Anomaly Detection Using Pre-Trained Deep Convolutional Neural Nets and Context Mining

Authors: Chongke Wu, Sicong Shao, Cihan Tunc, Salim Hariri

Abstract: Anomaly detection is critically important for intelligent surveillance systems to detect in a timely manner any malicious activities. Many video anomaly detection approaches using deep learning methods focus on a single camera video stream with a fixed scenario. These deep learning methods use large-scale training data with large complexity. As a solution, in this paper, we show how to use pre-tra… ▽ More Anomaly detection is critically important for intelligent surveillance systems to detect in a timely manner any malicious activities. Many video anomaly detection approaches using deep learning methods focus on a single camera video stream with a fixed scenario. These deep learning methods use large-scale training data with large complexity. As a solution, in this paper, we show how to use pre-trained convolutional neural net models to perform feature extraction and context mining, and then use denoising autoencoder with relatively low model complexity to provide efficient and accurate surveillance anomaly detection, which can be useful for the resource-constrained devices such as edge devices of the Internet of Things (IoT). Our anomaly detection model makes decisions based on the high-level features derived from the selected embedded computer vision models such as object classification and object detection. Additionally, we derive contextual properties from the high-level features to further improve the performance of our video anomaly detection method. We use two UCSD datasets to demonstrate that our approach with relatively low model complexity can achieve comparable performance compared to the state-of-the-art approaches. △ Less

Submitted 5 October, 2020; originally announced October 2020.

Comments: Accepted by AICCSA 2020

Optimal Transmission Policies for Energy Harvesting Age of Information Systems with Battery Recovery

Authors: Caglar Tunc, Shivendra Panwar

Abstract: We consider an energy harvesting information update system where a sensor is allowed to choose a transmission mode for each transmission, where each mode consists of a transmission power-error pair. We also incorporate the battery phenomenon called battery recovery effect where a battery replenishes the deliverable energy if kept idle after discharge. For an energy-limited age of information (AoI)… ▽ More We consider an energy harvesting information update system where a sensor is allowed to choose a transmission mode for each transmission, where each mode consists of a transmission power-error pair. We also incorporate the battery phenomenon called battery recovery effect where a battery replenishes the deliverable energy if kept idle after discharge. For an energy-limited age of information (AoI) system, this phenomenon gives rise to the interesting trade-off of recovering energy after transmissions, at the cost of increased AoI. Considering two metrics, namely peak-age hitting probability and average age as the worst-case and average performance indicators, respectively, we propose a framework that formulates the optimal transmission scheme selection problem as a Markov Decision Process (MDP). We show that the gains obtained by considering both battery dynamics and adjustable transmission power together are much higher than the sum gain achieved if they are considered separately. We also propose a simple methodology to optimize the system performance taking into account worst-case and average performances jointly. △ Less

Submitted 12 December, 2019; originally announced December 2019.

Comments: Submitted for publication