Pith Number

pith:TAP35CVE

pith:2026:TAP35CVEILSXWKS7K7ZXRQQCIX

not attested not anchored not stored refs resolved

On the Complexity of Checking Soundness of Natural Reductions (Extended Version)

Azadeh Farzan, Constantin Enea, Dominik Klumpp

Deciding whether a natural reduction is sound with respect to a commutativity relation is coNP-hard even for locking synchronization.

arxiv:2605.13780 v1 · 2026-05-13 · cs.PL

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{TAP35CVEILSXWKS7K7ZXRQQCIX}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

The problem of deciding whether a given natural reduction is sound with respect to a given (semi-)commutativity relation is coNP-hard already for a simple synchronization mechanism like locking.

C2weakest assumption

The reductions are purely syntactic (atomic blocks and global rendezvous points inserted into the thread template) and the commutativity relation is given as input; if real programs require more complex or data-dependent synchronization, the hardness result may not directly apply.

C3one line summary

Natural reductions for concurrent programs admit a sound-and-complete polynomial-time soundness check without synchronization but are coNP-hard under locking.

References

20 extracted · 20 resolved · 0 Pith anchors

[1] Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: ESOP. pp. 290–309. Lecture Notes in Com- puter Science, Springer (2013). https://doi. 2013 · doi:10.1007/978-3-642-37036-6_17

[2] Chajed, T., Kaashoek, M.F., Lampson, B.W., Zeldovich, N.: Verifying concurrent software using movers in CSPEC. In: OSDI. pp. 306–322. USENIX Association (2018) 2018

[3] Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: PODC. pp. 44–65. ACM (1988). https://doi.org/10. 1145/62546.62556 1988

[4] In: The Book of Traces, pp 1995 · doi:10.1142/9789814261456_

[5] Damian, A., Dragoi, C., Militaru, A., Widder, J.: Communication-closed asyn- chronous protocols. In: CAV (2). pp. 344–363. Lecture Notes in Computer Science, Springer (2019). https://doi.org/10.1007/9 2019 · doi:10.1007/978-3-030-25543-5_20

Receipt and verification

First computed	2026-05-18T02:44:15.741774Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

981fbe8aa442e57b2a5f57f378c20245c305359d59269cf3b6f7ec281e6221d0

Aliases

arxiv: 2605.13780 · arxiv_version: 2605.13780v1 · doi: 10.48550/arxiv.2605.13780 · pith_short_12: TAP35CVEILSX · pith_short_16: TAP35CVEILSXWKS7 · pith_short_8: TAP35CVE

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/TAP35CVEILSXWKS7K7ZXRQQCIX \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 981fbe8aa442e57b2a5f57f378c20245c305359d59269cf3b6f7ec281e6221d0

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "1936d50d3f00e4730ef20978b2e9193663ae31128ebd88edfdd6a2e7581507c8",
    "cross_cats_sorted": [],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.PL",
    "submitted_at": "2026-05-13T17:01:51Z",
    "title_canon_sha256": "c010cb65498f6b0eb37f740495c66e88ce2b7affa13a632dfdfe6850f49777b9"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.13780",
    "kind": "arxiv",
    "version": 1
  }
}