## 3 Proposed Algorithm for the Generalized Local \(I_{i}\)-Mutual Inclusion
\right.\) \(ts_{i}:\)integer, initially \(0\); \(nGrants_{i}\): integer, initially \(0\); \(gantedTo_{i}\): set of (integer, processID), initially\(\{(0,P_{j}\in\mathcal{CS}_{i}(C_{0}))\}\); pendingReq_: set of (integer, processID), initially\(\mathcal{O}\); preemptingNow\({}_{i}\): processID, initially nil;
```  
**Algorithm 1** Local variables for process \(P_{i}\) in algorithm \(l_{i}\)-LMUTIN```
**Exit-Sequence:**  
\(ts_{i}:=ts_{i}+1\);  
\(nGrants_{i}:=0\);  
for-each \(P_{j}\in(N_{i}\cup\{P_{i}\})\) send\(\langle\text{Request},ts_{i},P_{i}\rangle\)to\(P_{j}\);  
wait until\((nGrants_{i}=|N_{i}|+1)\);  
\(state_{i}:=\text{OutCS}\);  
Entry-Sequence:  
\(state_{i}:=\text{InCS}\);  
for-each \(P_{j}\in(N_{i}\cup\{P_{i}\})\) send\(\langle\text{Release},P_{i}\rangle\)to\(P_{j}\);  
On receipt of a\(\langle\text{Request},ts_{j},P_{j}\rangle\)message:  
\(pendingReq_{i}:=pendingReq_{i}\cup\{(ts_{j},P_{j})\}\);  
if\((|\text{generatedTo}_{i}|<|N_{i}|-i+1)\{(ts_{h},P_{h}):=deleteMin(pendingReq_{i})\);  
\(grantTo_{i}:=grantTo_{i}\cup\{(ts_{h},P_{h})\}\);  
send\(\langle\text{Grant}\rangle\) to \(P_{h}\);  
} elseif\((pemptingNow_{i}=\text{nil})\{(ts_{h},P_{h}):=max( grantedTo_{i})\);  
if\(((ts_{j},P_{j})<(ts_{h},P_{h}))\{\)  
\(pemptingNow_{i}:=P_{h}\);  
send\(\langle\text{Preempt},P_{i}\rangle\)to\(P_{h}\);  
```

**Algorithm 2** Algorithm \(l_{i}\)-LMUTIN: exit-sequence, entry-sequence and message handlers. ### Proof of Correctness

In this subsection, we show the correctness of \(l_{i}\)-LMUTIN. **Lemma 1**. : _(Safety) For each process \(P_{i}\in V\), \(l_{i}\leq|\mathcal{CS}_{i}(\text{C})|\leq|N_{i}|+1\) holds at any configuration \(\text{C}\)._Proof. : We assume that the initial configuration \(C_{0}\) is safe, i.e., \(l_{i}\leq|\mathcal{CS}_{i}(C_{0})|\). Therefore, we consider the process \(P_{i}\), which becomes unsafe first for the contrary. Suppose that \(|\mathcal{CS}_{i}(C)|<l_{i}\), that is \(|\overline{\mathcal{CS}_{i}(C)}|>|N_{i}|+1-l_{i}\). Because \(|\mathcal{CS}_{i}(C_{0})|\geq l_{i}\), consider a process \(P_{j}\in N_{i}\cup\{P_{i}\}\), which became the \(\mathsf{OutCS}\) state by the \((|N_{i}|+2-l_{i})\)-th lowest timestamp among processes in \(\overline{\mathcal{CS}_{i}(C)}\). Then, \(P_{j}\) obtains permission to be the \(\mathsf{OutCS}\) state from each process in \(N_{j}\cup\{P_{j}\}\). This implies that \(P_{i}\) receives a request \(\langle\mathsf{Request},ts_{j},P_{j}\rangle\) from \(P_{j}\) and that \(P_{i}\) sends a permission \(\langle\mathsf{Grant}\rangle\) to \(P_{j}\). Because \(P_{i}\) grants at most \(|N_{i}|+1-l_{i}\) permissions to exit the CS at each time, \(P_{j}\) cannot obtain a permission from \(P_{i}\); this is a contradiction. **Lemma 2**. : _(Liveness) Each process \(P_{i}\) changes into the \(\mathsf{InCS}\) and \(\mathsf{OutCS}\) states alternately infinitely often._

Proof. : By contrast, suppose that some processes do not change into the \(\mathsf{InCS}\) and \(\mathsf{OutCS}\) states alternately infinitely often. Let \(P_{i}\) be such a process where the lowest timestamp value for its request to be the \(\mathsf{OutCS}\) state is \((ts_{i},P_{i})\). Without loss of generality, we assume that \(P_{i}\) is blocked in the \(\mathsf{InCS}\) state. That is, \(P_{i}\) is blocked by the wait until statement in the exit-sequence (recall that each process changes into the \(\mathsf{InCS}\) state eventually when it is in the \(\mathsf{OutCS}\) state). Let \(P_{j}\) be any process in \(N_{i}\). * Suppose that \(P_{j}\) changes into the \(\mathsf{InCS}\) and \(\mathsf{OutCS}\) states alternately infinitely often. After \(P_{j}\) receives the \(\langle\mathsf{Request},ts_{i},P_{i}\rangle\) message from \(P_{i}\), the value of \((ts_{j},P_{j})\) exceeds the timestamp \((ts_{i},P_{i})\) for \(P_{i}\)'s request. Because, by this algorithm, the request with the lowest timestamp is granted preferentially, it is impossible for \(P_{j}\) to change into the \(\mathsf{InCS}\) and \(\mathsf{OutCS}\) states alternately infinitely often.