{'fraction_non_alphanumeric': 0.023462783171521034, 'fraction_numerical': 0.0, 'mean_word_length': 5.579787234042553, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On Justifying and Verifying Relaxed Detection of Conflicts in Concurrent Programs

Transactional Memory (TM) simplifies concurrent programming by providing atomic, compositional blocks within which programmers can reason sequentially. Many transactions have an access pattern where, initially, a large portion of the shared data is read, local computations is performed, and, later, a small portion of shared data is updated. Such transactions conflict frequently and result in poor performance. TM implementers have developed mechanisms for programmer-directed relaxed conflict detection. The programmer indicates to the TM to ignore certain conflicts. As a result, the frequency of conflict is reduced and performance approximates hand-craftedfine-grain concurrency. However, the clean, sequential, atomic compositional block simplicity of TM is lost. In this paper, we present a method for abstracting in a quantified manner the accesses on which conflicts are ignored. This abstraction, and a soundness theorem we state and prove, allow the programmer to reason sequentially on an abstracted version of the transaction. Properties proved on this abstract but sequential version of the transaction carry over to the original program.