Sharding is a technique to speed up transaction processing in blockchains, where the n processing nodes in the blockchain are divided into s disjoint groups (shards) that can process transactions in parallel. We study dynamic scheduling problems on a shard graph G_s where transactions arrive online over time and are not known in advance. Each transaction may access at most k shards, and we denote by d the worst distance between a transaction and its accessing (destination) shards (the parameter d is unknown to the shards). To handle different values of d, we assume a locality sensitive decomposition of G_s into clusters of shards, where every cluster has a leader shard that schedules transactions for the cluster. We first examine the simpler case of the stateless model, where leaders are not aware of the current state of the transaction accounts, and we prove a O(d log² s ⋅ min{k, √s}) competitive ratio for latency. We then consider the stateful model, where leader shards gather the current state of accounts, and we prove a O(log s⋅ min{k, √s}+log² s) competitive ratio for latency. Each leader calculates the schedule in polynomial time for each transaction that it processes. We show that for any ε > 0, approximating the optimal schedule within a (min{k, √s})^{1 -ε} factor is NP-hard. Hence, our bound for the stateful model is within a poly-log factor from the best possibly achievable. To the best of our knowledge, this is the first work to establish provably efficient dynamic scheduling algorithms for blockchain sharding systems.

Abstract Federated learning (FL) is a machine learning setting where clients keep the training data decentralized and collaboratively train a model either under the coordination of a central server (centralized FL) or in a peer-to-peer network (decentralized FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralized and a decentralized one, using the Communicating Sequential Processes (CSP) calculus and the Process Analysis Toolkit (PAT) model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freedom (safety property) and successful termination (reachability and liveness property). The CSP models are constructed as a faithful representation of the real Python code and are expressed directly in CSP# language that PAT uses. Then they are automatically checked top-down by PAT. The Python code follows a restricted actor-based programming model, and the construction of CSP# code from such Python code is performed systematically. The process is described in detail, ensuring that the models correspond to the actual code. It represents a basis for developing tools for automatic translation of certain classes of Python code to CSP models, expressed in CSP#.

Transactional memory is designed for developing parallel programs and improving the efficiency of parallel pro-grams. PSTM (python software transactional memory) mainly supports multi-core parallel programs based on the python language. In order to better adapt to the developing requirements of distributed concurrent programs and enhance the safety of the system, DPSTM (distributed python software transactional memory) was developed. Compared with PSTM, DPSTM has the advantages of higher operating efficiency and stronger fault tolerance. In this paper, we apply CSP (Communicating Sequential Processes) to formally analyze the components of DPSTM v2 architecture, the data exchange process between components, and two different transaction processing modes. We use the model checker PAT (Process Analysis Toolkit) to model the DPSTM v2 architecture and verify eight properties, including deadlock freedom, ACI (atomicity, isolation, and consistency), sequential consistency, data server availability, read tolerance, and crash tolerance. The verification results show that the DPSTM v2 archi-tecture can guarantee all of the above properties. In particular, the normal operation of the system can be maintained when some of the data servers are crashed, ensuring the safety of a distributed system.

We investigate scheduling algorithms for distributed transactional memory systems where transactions residing at nodes of a communication graph operate on shared, mobile objects. A transaction requests the objects it needs, executes once those objects have been assembled, and then sends the objects to other waiting transactions. We study scheduling algorithms with provable performance guarantees. Previously, only the offline batch scheduling setting was considered in the literature where transactions and the objects they access are known a priori. Minimizing execution time, even for the offline batch scheduling, is known to be NP-hard for arbitrary communication graphs. In this paper, we analyze for the very first time scheduling algorithms in the online dynamic scheduling setting where transactions and the objects they access are not known a priori and the transactions may arrive online over time. We provide efficient and near-optimal execution time schedules for dynamic scheduling in many specialized network architectures. The core of our technique is a method to convert offline schedules to online. We first describe a centralized scheduler which we then adapt it to a purely distributed scheduler. To our knowledge, these are the first attempts to obtain provably efficient online execution schedules for distributed transactional memory.

Starting with the analysis of the source codes of the Python Software Transactional Memory (PSTM) architecture, this paper applies process algebra CSP to formally verify the architecture at a fine-grained level. We analyze the communication process and components of the architecture from multiple perspectives and establish models describing the communication behaviors of the PSTM architecture. We use model checker PAT to automatically simulate and verify the established model. After adapting the traditional transactional properties to the PSTM architecture, we analyze and verify five properties for the PSTM architecture, including deadlock freeness, atomicity, isolation, consistency and optimism. The verification results indicate that all the properties are valid. Based on the judgement of the execution logic of the communication procedure in the PSTM architecture, we can conclude that the architecture can have a proper communication and can guarantee atomicity, isolation, consistency and optimism. Besides, we also provide a case study with an application scenario and propose a corollary that the value of the shared counter is equal to the number of parallel processes. We verify whether the case study system can satisfy all the conditions of corollary from both positive and negative perspectives. The results show that the corollary is tenable.

Transaction Memory (TM) is designed for simplifying parallel programming, while some key problems exist in it, such as starvation and reduced performance with high contention among transactions. In order to improve the performance of TM, researchers have designed several transaction scheduling algorithms and given their experimental results. However, the evaluations on the algorithms given by these researches are rather partial and lack of generality. Since these experimental results ignore the verification of properties which are necessary for transaction scheduling and could be greatly affected by the execution environment, thus it is still challenging for us to judge the quality of the algorithms for TM. In this paper, we provide a formal approach to evaluate transaction scheduling algorithms in a more comprehensive and strict way. We choose three recently proposed algorithms as motivating examples and formalize them using the process algebra CSP. We also use a model checker PAT to verify the properties (e.g., deadlock freeness and starvation freeness) of the models. Besides, it is also easier to compare the performance of the algorithms, from the perspective of makespan, speedup, aborts time and throughput, based on the statistics given by PAT. Consequently, a formal approach can be achieved to evaluate transaction scheduling algorithms, which is also a good guide for the further design of the algorithms for TM.

Automotive industry is one of the fastest growing fields adopting the information and communication technologies (ICT). Responding to the needs of the automotive industry requires improving the education in ICT fields. This paper describes the recently started project with goals to modernize laboratories and develop graduate-level curriculum and study materials for automotive software engineering.

Python Software Transactional Memory (PSTM), was proposed to break the limiting factors which restrict diffusion of the TM paradigm into more application fields. Since the widespread use of the PSTM, it is of great significance to formally analyze and verify relevant transactional properties of this architecture. In this paper, we apply Communicating Sequential Processes (CSP) to model the PSTM. Moreover, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for some relevant properties, e.g. ACID. Our modeling and verification show that the PSTM can guarantee some transactional properties.

We investigate scheduling algorithms for distributed transactional memory systems where transactions residing at nodes of a communication graph operate on shared, mobile objects. A transaction requests the objects it needs, executes once those objects have been assembled, and then possibly forwards those objects to other waiting transactions. Minimizing execution time in this model is known to be NP-hard for arbitrary communication graphs, and also hard to approximate within any factor smaller than the size of the graph. Nevertheless, networks on chips, multi-core systems, and clusters are not arbitrary. Here, we explore efficient execution schedules in specialized graphs likely to arise in practice: Clique, Line, Grid, Cluster, Hypercube, Butterfly, and Star. In most cases, when individual transactions request k objects, we obtain solutions close to a factor O(k) from optimal, yielding near-optimal solutions for constant k. These execution times approximate the TSP tour lengths of the objects in the graph. We show that for general networks, even for two objects (k=2), it is impossible to obtain execution time close to the objects' optimal TSP tour lengths, which is why it is useful to consider more realistic network models. To our knowledge, this is the first attempt to obtain provably fast schedules for distributed transactional memory.

In millimeter wave networks, a received signal level and interference dynamically vary due to rain attenuation. These physical layer variations have influence on upper communication layers, which yield to variable network capabilities to serve traffic demands. Standards and agreements between service providers and users usually specify performance objectives at annual level. In order to make realistic annual level performance analysis of such networks, a new computationally efficient dynamic rain attenuation model is proposed and analyzed. The model reproduces assumed rain statistics at annual level: cumulative distribution function (cdf) of rain intensity, number of rain events in which specified rain intensity threshold is exceeded, rain advection vector intensity, and rain advection vector azimuth. Derivation of model parameter tolerances is based on the experimental results from dense rain gauge network. As an example of model application, annual level cdfs of node-to-node connection capacity in a test network are calculated.

This paper investigates the use of flow size distribution as a source in entropy-based detection. The performance of detection based on this distribution is compared with the performance of detection based on simple packet distribution, namely distribution of addresses, which outperforms other simple distributions in detection of distributed denial-of-service attacks. The following parameters are compared: true and false positive rate and detection delay. The dependence of the aforementioned parameters on detection threshold is given. The results for detection delay show that two detectors are very close with respect to this feature. Regarding the detection rate, experiments show that in most cases, the performance of flow-size based detector is superior to the performance of address-based detector. Copyright © 2015 John Wiley & Sons, Ltd.

Reliable packet delivery within stringent delay constraints is of paramount importance to mission-critical computer applications with hard real-time constraints. Because retransmission and coding techniques counteract the delay requirements, reliability may be achieved through replication over multiple fail-independent paths. The existing solutions, such as the parallel redundancy protocol (PRP), replicate all packets at the media access control layer over parallel paths. PRP works best in local area networks; however, it is not viable for IP networks that are a key element of emerging mission-critical systems. This limitation, coupled with diagnostic inability and lack of security, renders PRP unsuitable for reliable data delivery in these IP networks. To address this issue, we present a transport-layer solution: the IP parallel redundancy protocol (iPRP). Designing iPRP poses nontrivial challenges in the form of selective packet-replication, and soft-state and multicast support. iPRP replicates only time-critical unicast or multicast user datagram protocol traffic. iPRP requires no modifications to the existing monitoring application, end-device operating system, or to the intermediate network devices. It only requires a simple software installation on the end devices. iPRP has a set of diagnostic tools for network debugging. With our implementation of iPRP in Linux, we show that iPRP supports multiple flows with minimal processing-and-delay overhead. It is being installed in our campus smart-grid network and is publicly available.

We consider scheduling problems in the data flow model of distributed transactional memory. Objects shared by transactions move from one network node to another by following network paths. We examine how the objects' transfer in the network affects the completion time of all transactions and the total communication cost. We show that there are problem instances for which there is no scheduling algorithm that can simultaneously minimize the completion time and communication cost. These instances reveal a trade-off, minimizing execution time implies high communication cost and vice versa. On the positive side, we provide scheduling algorithms which are independently communication cost near-optimal or execution time efficient.

Reliable packet delivery within stringent delay constraints is of primal importance to industrial processes with hard real-time constraints, such as electrical grid monitoring. Because retransmission and coding techniques counteract the delay requirements, reliability is achieved through replication over multiple fail-independent paths. Existing solutions such as parallel redundancy protocol (PRP) replicate all packets at the MAC layer over parallel paths. PRP works best in local area networks, e.g., sub-station networks. However, it is not viable for IP layer wide area networks which are a part of emerging smart grids. Such a limitation on scalability, coupled with lack of security, and diagnostic inability, renders it unsuitable for reliable data delivery in smart grids. To address this issue, we present a transport-layer design: IP parallel redundancy protocol (iPRP). Designing iPRP poses non-trivial challenges in the form of selective packet replication, soft-state and multicast support. Besides unicast, iPRP supports multicast, which is widely using in smart grid networks. It duplicates only time-critical UDP traffic. iPRP only requires a simple software installation on the end-devices. No other modification to the existing monitoring application, end-device operating system or intermediate network devices is needed. iPRP has a set of diagnostic tools for network debugging. With our implementation of iPRP in Linux, we show that iPRP supports multiple flows with minimal processing and delay overhead. It is being installed in our campus smart grid network and is publicly available.

Abstract This paper presents an evaluation of entropy‐based network intrusion detection in the case of outbound denial‐of‐service attacks in edge networks. The detector monitors entropy of several simple packet distributions: source and destination ports, and number of packets and bytes transferred. Cumulative sum control chart (CUSUM) algorithm is used for change‐point detection. The performance of entropy‐based method has been evaluated in simulated environment, using ns2 simulator, and compared with an optimized version of one existing approach, namely CUSUM‐based monitoring of the number of Synchronize sequence numbers (SYN) packets. The results show that entropy‐based detector does not reach the performance of a method tailored for a specific type of attack but, in general case, has good performance. The main advantage of entropy‐based detector is its generality, as it supports detection of many different types of attacks and network anomalies. Copyright © 2014 John Wiley & Sons, Ltd.

Abstract In this paper, we present results of application of Tsallis entropy in detection of denial of service attacks. Two detectors, one based on Tsallis and the other one based on Shannon's entropy, have been applied in several attack simulations, and their properties have been compared. The simulated attack is Synchronize packet (SYN) flood. A simple packet distribution, that is, entropy of source addresses are considered. In both cases, cumulative sum control chart algorithm is used for change point detection. Properties of two detectors that are compared are detection delay and rate of true and false positives. The results show that Tsallis entropy‐based detector can outperform (with respect to false positive rate) Shannon‐based one but that requires careful tuning of TsallisQparameter that depends on characteristics of network traffic. The detection delay of two detectors is approximately the same. Copyright © 2015 John Wiley & Sons, Ltd.

Multipath TCP (MPTCP) has been proposed recently as a mechanism for transparently supporting multiple connections to the application layer. It is under discussion at the IETF. We nevertheless demonstrate that the current MPTCP suffers from two problems: P1) Upgrading some TCP users to MPTCP can reduce the throughput of others without any benefit to the upgraded users, which is a symptom of not being Pareto-optimal; and P2) MPTCP users could be excessively aggressive toward TCP users. We attribute these problems to the linked-increases algorithm (LIA) of MPTCP and, more specifically, to an excessive amount of traffic transmitted over congested paths. The design of LIA forces a tradeoff between optimal resource pooling and responsiveness. We revisit the problem and show that it is possible to provide these two properties simultaneously. We implement the resulting algorithm, called the opportunistic linked-increases algorithm (OLIA), in the Linux kernel, and we study its performance over our testbed by simulations and by theoretical analysis. We prove that OLIA is Pareto-optimal and satisfies the design goals of MPTCP. Hence, it can avoid the problems P1 and P2. Our measurements and simulations indicate that MPTCP with OLIA is as responsive and nonflappy as MPTCP with LIA and that it solves problems P1 and P2.

MPTCP has been proposed recently as a mechanism for supporting transparently multiple connections to the application layer. It is under discussion at the IETF. We show, however, that the current MPTCP suffers from two problems: (P1) Upgrading some TCP users to MPTCP can reduce the throughput of others without any benefit to the upgraded users, which is a symptom of not being Pareto-optimal; and (P2) MPTCP users could be excessively aggressive towards TCP users. We attribute these problems to the linked-increases algorithm (LIA) of MPTCP and, more specifically, to an excessive amount of traffic transmitted over congested paths.

Abstract In this paper we present a case study of the software maintenance practice that has been successfully applied to real‐time distributed systems, which are installed and fully operational in Moscow, St. Petersburg, and other cities across Russia. In this paper we concentrate on the software maintenance process, including customer request servicing, in‐field error logging, role of information system, software deployment, and software quality policy, and especially the software quality prediction process. In this case study, the prediction process is shown to be integral and one of the most important parts of the software maintenance process. We include a software quality prediction procedure overview and an example of the actual practice. The quality of the new software update is predicted on the basis of the current update's quantity metrics data and quality data, and new update's quantity metrics data. For management, this forecast aids software maintenance efficiency, and cost reduction. For practitioners, the most useful result presented is the process for determining the value for the break point. We end this case study with five lessons learned. Copyright © 2001 John Wiley & Sons, Ltd.

The authors present the software reliability and maintenance concept, which is used in the software development, testing, and maintenance process, for automatic call distributor MEDIO ACD. The concept has been successfully applied on systems, which are installed and fully operational in Moscow and Saint Petersburg, Russia. The authors concentrate on two main issues: (i) set of fault-tolerant mechanisms needed for the system exploitation (error logging, checkpoint-restart, overload protection and tandem configuration support); (ii) MEDIO ACD software maintenance concept, in which the quality of the new software update is predicted on the basis of the current update's metrics and quality, and the new update's metrics. This forecast aids software maintenance efficiency, and cost reduction.

The paper presents a software development and testing methodology, which was used for the new version of the subscriber digital concentrator ACK-2000. This concentrator was developed for the Russian telecommunication network. During the development process special attention was paid to precise software specification, professional implementation, and testing/redesign, in order to reach the given criterion of 0.1% of unsuccessful calls. The tests, which were conducted, include functional tests and real-time load tests, with the real exchange and the call generator connected to the subscriber lines. The results of these tests and software reliability analysis are reported.