More Like this

1. Proceedings of the 2025 SIAM International Meshing Roundtable; Parallelization of the Finite Element-based Mesh Warping Algorithm Using Hybrid Parallel Programming

   https://doi.org/10.1137/1.9781611978575.12  

   Haque, Abir; Shontz, Suzanne M (March 2025, Society for Industrial and Applied Mathematics)

   Si, Hang; Shepherd, Kendrick M; Zhang, Yongjie Jessica (Ed.)

   Warping large volume meshes has applications in biomechanics, aerodynamics, image processing, and cardiology. However, warping large, real-world meshes is computationally expensive. Existing parallel implementations of mesh warping algorithms do not take advantage of shared-memory and one-sided communication features available in the MPI-3 standard. We describe our parallelization of the finite element-based mesh warping algorithm for tetrahedral meshes. Our implementation is portable across shared and distributed memory architectures, as it takes advantage of shared memory and one-sided communication to precompute neighbor lists in parallel. We then deform a mesh by solving a Poisson boundary value problem and the resulting linear system, which has multiple right-hand sides, in parallel. Our results demonstrate excellent efficiency and strong scalability on up to 32 cores on a single node. Furthermore, we show a 33.9% increase in speedup with 256 cores distributed uniformly across 64 nodes versus our largest single node speedup while observing sublinear speedups overall. 

   more » « less
2. Application of Graph Sparsification in Developing Parallel Algorithms for Updating Dynamic Networks

   Srinivasan, S; Das, S; Bhowmick, S (May 2016, Graph Algorithms Building Blocks (GABB’2016))

   Analyzing large dynamic networks is an important problem with applications in a wide range of disciplines. A key operation is updating the network properties as its topology changes. In this paper we present graph sparsification as an efficient abstraction for updating the properties of dynamic networks. We demonstrate the applicability of graph sparsification in updating the connected components in random and scalefree networks on shared memory systems. Our results show that the updating is scalable (10X on 16 processors for larger networks). To the best of our knowledge this is the first parallel implementation of graph sparsification. Based on these initial results, we discuss how the current implementation can be further improved and how graph sparsification can be applied to updating other network properties. 

   more » « less
3. Resilient Distributed Causal Memory in Client-Server Model

   https://doi.org/10.1109/PRDC47002.2019.00035  

   Tseng, Lewis Wang (December 2019, 24th IEEE Pacific Rim International Symposium on Dependable Computing)

   We study distributed causal shared memory (or key- value pairs) in an asynchronous network under crash failures. Causal memory, introduced by Ahamad et al. in the context of multi-processor environment in 1994, is an abstraction which ensures that nodes agree on the relative ordering of read and write operations that are causally related on key-value pairs. Inspired by the recent interests in geo-replicated causal storage systems (e.g., COPS, Eiger, Bolt-on), we systematically study the fault-tolerance property of the causal shared memory in the client-server model in this work. We identify that 2f + 1 servers is both necessary and sufficient to build a resilient causal memory in the presence of up to f crashed servers. We provide both the necessity proof and a new optimal algorithm that matches the bound. For evaluation, we implement our algorithm in Golang and compare the perfor- mance with state-of-the-art fault-tolerant algorithms that ensure atomicity in the Google Cloud Platform. 

   more » « less
4. Cache Coherence Over Disaggregated Memory

   https://doi.org/10.14778/3746405.3746422  

   Wang, Ruihong; Wang, Jianguo; Aref, Walid G (May 2025, Proceedings of the VLDB Endowment)

   Disaggregating memory from compute offers the opportunity to better utilize stranded memory in cloud data centers. It is important to cache data in the compute nodes and maintain cache coherence across multiple compute nodes. However, the limited computing power on disaggregated memory servers makes traditional cache coherence protocols suboptimal, particularly in the case of stranded memory. This paper introduces SELCC; a Shared-Exclusive Latch Cache Coherence protocol that maintains cache coherence without imposing any computational burden on the remote memory side. It aligns the state machine of the shared-exclusive latch protocol with the MSI protocol, thereby ensuring both atomicity of data access and cache coherence with sequential consistency. SELCC embeds cache-ownership metadata directly into the RDMA latch word, enabling efficient cache ownership management via RDMA atomic operations. SELCC can serve as an abstraction layer over disaggregated memory with APIs that resemble main-memory accesses. A concurrent B-tree and three transaction concurrency control algorithms are realized using SELCC's abstraction layer. Experimental results show that SELCC significantly outperforms RPC-based protocols for cache coherence under limited remote computing power. Applications on SELCC achieve comparable or superior performance over disaggregated memory compared to competitors. 

   more » « less
5. Structural temporal logic for mechanized program verification

   Ioannidis, Eleftherios; Zakowski, Yannick; Zdancewic, Steve; Angel, Sebastian (October 2025, Proceedings of the ACM on programming languages)

   Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using Ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio. 

   more » « less