Search for: All records

Abstract: Morgan and Parker proved that if G is a group with Z(G)=1, then the connected components of the commuting graph of G have diameter at most 10. Parker proved that if, in addition, G is solvable, then the commuting graph of G is disconnected if and only if G is a Frobenius group or a 2-Frobenius group, and if the commuting graph of G is connected, then its diameter is at most 8. We prove that the hypothesis Z (G) = 1 in these results can be replaced with G' \cap Z(G)=1. We also prove that if G is solvable and G/Z(G) is either a Frobenius group or a 2-Frobenius group, then the commuting graph of G is disconnected. 

Abstract: For a group G, we define a graph Delta (G) by letting G^#=G\{1} be the set of vertices and by drawing an edge between distinct elements x,y in G^# if and only if the subgroup is cyclic. Recall that a Z-group is a group where every Sylow subgroup is cyclic. In this short note, we investigate Delta (G) for a Z-group G. 

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) and reduce the complex dependencies among components at different levels of abstraction. Despite their obvious importance, concurrent abstraction layers have not been treated formally. This severely limits the applicability of layer-based techniques and makes it difficult to scale verification across multiple concurrent layers. In this paper, we present CCAL---a fully mechanized programming toolkit developed under the CertiKOS project---for specifying, composing, compiling, and linking certified concurrent abstraction layers. CCAL consists of three technical novelties: a new game-theoretical, strategy-based compositional semantic model for concurrency (and its associated program verifiers), a set of formal linking theorems for composing multithreaded and multicore concurrent layers, and a new CompCertX compiler that supports certified thread-safe compilation and linking. The CCAL toolkit is implemented in Coq and supports layered concurrent programming in both C and assembly. It has been successfully applied to build a fully certified concurrent OS kernel with fine-grained locking.