FPTLin

Fixed parameter tractable algorithms for monitoring linearizability for concurrent histories. Based on the following paper:

Zheng Han Lee and Umang Mathur. 2026. Fixed Parameter Tractable Linearizability Monitoring. Proc. ACM Program. Lang. 10, PLDI, Article 237 (June 2026). https://doi.org/10.1145/3808315

Histories

Histories are text files that provide a data type as header and operations on a single object of the stated data type in the following rows. Yes, we assume all operations to be completed by the end of the history.

Data types are prefixed with # followed by any of the supported tags:

• stack
• queue
• priorityqueue
• rmw
• semaphore
• set

Operations are denoted by process id, start time, end time, method, and value(s) in that order. Refer to examples in testcases directory for supported methods and values for a given data type.

Example

# stack
0 1 5 PUSH 1
1 2 6 PUSH 2
2 3 7 POP 2
3 4 8 POP 1
4 2 9 PEEK -1

Usage

-bash-4.2$ ./fptlin [-tvh] <history_file>

Options

• -t: report time taken in seconds
• -v: print verbose information
• -h: include header
• --help: show help message

Output

The standard output shall be in the form:

"%d %f\n", <linearizability>, <time taken>

linearizability prints 1 when input history is linearizable, 0 otherwise.

-bash-4.2$ ./build/fptlin -t testcases/priorityqueue/lin_simple_0.log
1 1.8e-05

Time Complexity

n is the size of the given history and k is the number of processes

Data Type	Time Complexity
Stack	$O(2^{3k} \cdot n^3)$
Queue	$O(k2^{2k} \cdot n^2)$
Priority Queue	$O(k2^k \cdot n\log{n})$
Read-Modify-Write Register	$O(k2^k \cdot n + n\log{n})$
Non-blocking Semaphore	$O(k2^k \cdot n + n\log{n})$
Set	$O(k2^k \cdot n + n\log{n})$