Networked Systems: 8th International Conference, NETYS 2020, Marrakech, Morocco, June 3–5, 2020, Proceedings (Computer Communication Networks and Telecommunications)

This book constitutes the revised selected papers of the 8th International Conference on Networked Systems, NETYS 2020, held in Marrakech, Morocco, in June 2020.* The 18 revised full papers and 4 short papers presented together with 3 invited papers were carefully reviewed and selected from 46 submissions. The papers cover all aspects related to the design and the development of these systems, including, but not restricted to, concurrent and distributed algorithms, parallel/concurrent/distributed programming, multi-core architectures, formal verification, distributed databases, cloud systems, networks, security, formal verification, etc. *The conference was held virtually due to the COVID-19 pandemic. Preface Organization Abstracts Reasoning About Concurrent Data Types Security and Privacy for Distributed Optimization and Learning Contents Invited Papers On Network Topologies and the Decidability of Reachability Problem 1 Introduction 2 Distributed Systems, Topology, Reachability Problem 3 Boundaries of Decidability 4 Conclusions References Hide Me: Enabling Location Privacy in Heterogeneous Vehicular Networks 1 Introduction 2 System Model 3 Game-Theoretic Model for Privacy-Sensitive Communication 3.1 Game-Theoretic Solution 3.2 Deriving the Utility-Optimal Strategy 4 Evaluation 5 Conclusion References Blockchains and the Commons 1 Introduction 2 State of the Art 3 Explore Novel Models of Reliability for Blockchains 3.1 Blockchain Robustness to Dynamic Adversaries 3.2 Robustness to Rationality and Irrationality 4 Formal Abstractions for Blockchains Consistency 4.1 Defining New Consistency Abstractions for Blockchains 4.2 Design and Formally Prove New Consistency Algorithms Tolerant to Complex Behaviors 5 Develop Correct-by-Construction Agreement Algorithms for Blockchains 5.1 Feasibility of Blockchain Agreement Face to Complex Faults and Behaviors 5.2 New Abstractions for Blockchain Agreement 6 Develop Correct-by-Construction Overlays and Routing Algorithms for Blockchains 6.1 New Abstractions for Blockchain Overlays 6.2 New Formally Verified Routing Protocols for Blockchains 7 Blockchains Interoperability 8 Conclusions References Regular Papers On the State Reachability Problem for Concurrent Programs Under Power 1 Introduction 1.1 Related Work 2 Programming Model 2.1 Programs 2.2 Power Semantics 3 Undecidability 4 Conclusion References On the Encoding and Solving of Partial Information Games 1 Introduction 2 Preliminaries 3 Resolution of Partial Information Games, with Memoryless Strategies 3.1 Complexity Results 3.2 Encoding a Partial Information Game as a SAT Problem 4 Application: Automatic Synthesis of Strategies for Swarms of Autonomous Oblivious Robots 4.1 Model for the Robots 4.2 Definition of the Arena 5 Conclusion References Efficient Concurrent Execution of Smart Contracts in Blockchains Using Object-Based Transactional Memory 1 Introduction 2 System Model 3 Proposed Mechanism 3.1 The Block Graph 3.2 Multi-threaded Miner 3.3 Multi-threaded Validator 3.4 Detection of Malicious Miners by Smart Multi-threaded Validator (SMV) 4 Experimental Evaluation 5 Conclusion and Future Directions References Exploring IoT Trickle-Based Dissemination Using Timed Model-Checking and Symbolic Execution 1 Introduction 2 Network of Extended Timed Automata 3 Trickle Models 4 Exploring Trickle with UPPAAL and DIVERSITY 5 Conclusion References Broadcasting Information in Multi-hop Networks Prone to Mobile Byzantine Faults 1 Introduction 2 Related Works 3 System Model 3.1 Graph Metrics 4 Mobile Byzantine Reliable Communication Problem Specification 5 Reliable Communication in Asynchronous Systems 6 Reliable Communication in Synchronous Systems 6.1 Reliable Communication Correctness Conditions 6.2 Graph Parameters Comparison 7 Conclusion References Infinite Grid Exploration by Disoriented Robots 1 Introduction 2 Model 3 Impossibility Results 4 Infinite Grid Exploration with =1 4.1 An Algorithm Using Six Robots and Three Fixed Colors 4.2 An Algorithm Using Five Robots and Five Modifiable Colors 5 Infinite Grid Exploration with =2 and No Light 6 Conclusion and Perspectives References Wireless Broadcast with Short Labels 1 Introduction 2 Model and Problem Definition 3 Level-Separable Networks 3.1 Formal Definition of Level-Separable Networks 4 Broadcast in Level-Separable Network 4.1 Broadcast with 1-bit Labelling 4.2 1-bit Labelling Scheme LS 4.3 Correctness of Algorithm LS 5 Broadcast with ACK in Level-Separable Network 5.1 2-bits Labelling Broadcast with ACK 5.2 2-bits Labelling Scheme LSACK 5.3 Correctness of Algorithm LSACK 6 Hardness of Level Separation 7 Conclusion References The Imitation Game: Algorithm Selection by Exploiting Black-Box Recommenders 1 Introduction 2 RecRank 3 Evaluation 4 Related Work 5 Discussion and Limitations 6 Concluding Remarks References Byzantine k-Set Agreement 1 Introduction 2 Model and Definitions 2.1 Computation Models 2.2 The k-Set Agreement Problem 3 Algorithms 4 Impossibility 5 Conclusion References Fissile Locks 1 Introduction 2 The Fissile Algorithm 2.1 Specialized CNA 3 Related Work 4 Empirical Evaluation 4.1 MutexBench 4.2 Std::atomic 4.3 FIFO Support 5 Conclusion References Verifying Safety of Parameterized Heard-Of Algorithms 1 Introduction 2 Motivating Example 3 Heard-Of Programs 4 Symbolic Representation 5 A Symbolic Verification Procedure 6 Experimental Results 7 Conclusion and Future Work References Staleness and Local Progress in Transactional Memory 1 Introduction 2 Definitions 2.1 Basic TM Concepts 2.2 TM Consistency 2.3 Progress Conditions 3 Impossibility Result 3.1 Stale Values in TM 3.2 Impossibility of k-staleness and Local Progress 4 Discussion References Generic Framework for Optimization of Local Dissemination in Wireless Networks 1 Introduction 2 Model and Problems 2.1 Local Dissemination Problems 3 Generic Framework 3.1 Integer Linear Program Formulation 3.2 Correctness 4 Simulations 5 Discusion of Results and Conclusions References Verifying Weakly Consistent Transactional Programs Using Symbolic Execution 1 Introduction 2 Transactions on Weakly Consistent Systems 2.1 Abstract Executions 2.2 Axioms for Weak Consistency 2.3 Weak Consistency Models 3 Encoding Weakly Consistent Executions 3.1 Symbolic Execution of Transactions 3.2 Encoding the Executions 3.3 Encoding the Consistency Model 4 Experiments 5 Related Work 6 Conclusion References NetSheriff: Sheltering Software-Defined Networks from Rogue Switches 1 Introduction 2 Related Work 3 Motivation and Fault Scenarios 4 NetSheriff 5 Implementation 5.1 NetSight-Based Instrumentation 5.2 MAFIA-Based Instrumentation 5.3 Postcard Consolidation and Construction of `3́9`42`"̇613A``45`47`"603AGO 5.4 Differential Analysis 6 Evaluation 6.1 Proxy Overhead 6.2 Performance of the Differential Analysis 6.3 Error Identification 6.4 Overhead 7 Conclusions References Self-stabilizing Uniform Reliable Broadcast 1 Introduction 2 System Settings 3 Non-self-stabilizing URB Algorithms 4 Unbounded Self-stabilizing Uniform Reliable Broadcast 5 Correctness 6 Bounded Self-stabilizing Uniform Reliable Broadcast 7 Conclusions References Fully Anonymous Consensus and Set Agreement Algorithms 1 Introduction: Computing Model 1.1 On the Process Side 1.2 On the Memory Side 1.3 Motivation and Content of the Paper 2 Fully Anonymous Obstruction-Free Set Agreement Using RW Registers 2.1 A Fully Anonymous RW Set Agreement Algorithm 2.2 Proof of the Algorithm 3 Fully Anonymous Obstruction-Free Consensus Using RW Registers 4 Fully Anonymous Obstruction-Free Consensus Using RW/Snapshot Registers 4.1 A Fully Anonymous Consensus Algorithm 4.2 Proof of the Algorithm 5 Fully Anonymous Wait-Free Consensus Using RMW Registers 6 Conclusion References Cutoffs for Symmetric Point-to-Point Distributed Algorithms 1 Introduction 2 Motivating Example 3 Model of Computation 3.1 The Process Template 3.2 Modeling the Distributed System 4 Cutoff Results 4.1 Index Transpositions And symmetric point–to–point systems 4.2 Trace Equivalence of G2 and GN Under AP{1, 2} 4.3 Cutoff Results Of symmetric point–to–point algorithms 5 Experiments 6 Conclusion References Short Papers Stateless Distributed Ledgers 1 Introduction 2 Model 3 Examples of Stateless DLTs 4 Impossibility of Stateless Proof of Stake Blockchains References Stability Under Adversarial Injection of Dependent Tasks (Extended Abstract) 1 Introduction 2 Model 3 Our Results References Collaborative Filtering: Comparative Study Between Matrix Factorization and Neural Network Method 1 Introduction 2 Matrix Factorization vs Neural Network 2.1 Singular Value Decomposition (SVD) 2.2 Neural Collaborative Filtering 3 Experiments 3.1 Evaluation Metrics 3.2 Dataset 3.3 Comparing the Methods 4 Conclusion and Future Work References Routing in Generalized Geometric Inhomogeneous Random Graphs 1 Introduction 2 (,)-KG Model 3 Routing Algorithms 4 Experimental Evaluation References Author Index