Skip to content

Commit c68f4bf

Browse files
mchadalavadamchadalavada
authored
Add basic lock server example for pobserve (#898)
1 parent 1bb6707 commit c68f4bf

File tree

11 files changed

+80434
-0
lines changed

11 files changed

+80434
-0
lines changed

‎Src/PObserve/Examples/LockServerPObserve/.gitignore‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
.idea/
2+
spec/
3+
/build
4+
dependencies.*
5+
/dependencies
6+
compile.log
7+
.DS_Store

‎Src/PObserve/Examples/LockServerPObserve/README.md‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# LockServerPObserve
2+
3+
This project demonstrates the use of PObserve for monitoring a lock server implementation.
4+
5+
## Project Structure
6+
7+
- `src/main/java/` - Source code for the project
8+
- `src/test/java/` - Test code
9+
- `src/test/resources/` - Test resources including sample log files
10+
11+
## Building the Project
12+
13+
This project uses Gradle for build automation.
14+
15+
### Prerequisites
16+
17+
- Java Development Kit (JDK) 11 or later
18+
- Gradle 7.0 or later (or use the Gradle Wrapper)
19+
- P (>= 2.4.0)
20+
21+
### Commands
22+
Generate gradle wrapper:
23+
24+
```bash
25+
gradle wrapper
26+
```
27+
28+
To build the project:
29+
30+
```bash
31+
./gradlew build
32+
```
33+
34+
To run tests:
35+
36+
```bash
37+
./gradlew test
38+
```
39+
40+
Building the project will create the project jar in the `build/libs/` directory with the name `LockServerPObserve-1.0.0-uber.jar`.

‎Src/PObserve/Examples/LockServerPObserve/build.gradle.kts‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
2+
3+
plugins {
4+
id("java")
5+
id("java-library")
6+
id("com.github.johnrengelman.shadow") version "7.1.2"
7+
}
8+
9+
repositories {
10+
mavenLocal()
11+
mavenCentral()
12+
}
13+
14+
val pobserveVersion = "1.0.0"
15+
16+
dependencies {
17+
// PObserve dependencies
18+
implementation("io.github.p-org:pobserve-commons:1.0.0")
19+
implementation("io.github.p-org:pobserve-java-unit-test:1.0.0")
20+
21+
// Testing dependencies
22+
testImplementation("org.junit.jupiter:junit-jupiter-api:5.10.1")
23+
testImplementation("org.junit.jupiter:junit-jupiter-engine:5.10.1")
24+
testRuntimeOnly("org.junit.platform:junit-platform-launcher")
25+
}
26+
27+
sourceSets {
28+
main {
29+
java {
30+
srcDirs("src/main/java")
31+
}
32+
resources {
33+
srcDirs("src/main/resources")
34+
}
35+
}
36+
test {
37+
java {
38+
srcDirs("src/test/java")
39+
}
40+
resources {
41+
srcDirs("src/test/resources")
42+
}
43+
}
44+
}
45+
46+
tasks.test {
47+
useJUnitPlatform()
48+
testLogging {
49+
events("passed", "skipped", "failed")
50+
}
51+
}
52+
53+
tasks.register<Exec>("compilePSpec") {
54+
commandLine("p", "compile", "--mode", "pobserve")
55+
workingDir = File("${project.rootDir}/src/main")
56+
}
57+
58+
tasks.named("compileJava") {
59+
dependsOn("compilePSpec")
60+
}
61+
62+
tasks.named<ProcessResources>("processTestResources") {
63+
duplicatesStrategy = DuplicatesStrategy.EXCLUDE
64+
}
65+
66+
tasks.withType<ShadowJar> {
67+
archiveBaseName.set("LockServerPObserve")
68+
archiveClassifier.set("all")
69+
archiveVersion.set("1.0.0")
70+
mergeServiceFiles()
71+
}
72+
73+
// Task for creating the uber jar
74+
tasks.register<ShadowJar>("uberjar") {
75+
archiveBaseName.set("LockServerPObserve")
76+
archiveClassifier.set("uber")
77+
archiveVersion.set("1.0.0")
78+
from(sourceSets.main.get().output)
79+
from(sourceSets.test.get().output)
80+
configurations = listOf(
81+
project.configurations.runtimeClasspath.get(),
82+
project.configurations.testRuntimeClasspath.get()
83+
)
84+
mergeServiceFiles()
85+
exclude("META-INF/*.SF", "META-INF/*.DSA", "META-INF/*.RSA")
86+
}
87+
88+
group = "io.github.p-org"
89+
version = "1.0.0"

‎Src/PObserve/Examples/LockServerPObserve/src/main/PObserveDemo.pproj‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
<Project>
2+
<InputFiles>
3+
<PFile>./PSpec/</PFile>
4+
</InputFiles>
5+
<ProjectName>LockServerPObserve</ProjectName>
6+
<OutputDir>java/lockserver/pobserve/spec</OutputDir>
7+
<pobserve-package>lockserver.pobserve.spec</pobserve-package>
8+
</Project>

‎Src/PObserve/Examples/LockServerPObserve/src/main/PSpec/LockServerCorrect.p‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
type tLockReq = (clientId: tClientId, lockId: tLockId, rId: int);
2+
type tLockResp = (status: tLockRespStatus, clientId: tClientId, lockId: tLockId, lockStatus: tLockStatus, rId: int);
3+
type tReleaseReq = (clientId: tClientId, lockId: tLockId, rId: int);
4+
type tReleaseResp = (status: tReleaseRespStatus, clientId: tClientId, lockId: tLockId, lockStatus: tLockStatus, rId: int);
5+
type tLockId = int;
6+
type tClientId = int;
7+
8+
enum tLockStatus {
9+
LOCKED,
10+
FREE
11+
}
12+
13+
enum tLockRespStatus {
14+
LOCK_SUCCESS,
15+
LOCK_ERROR
16+
}
17+
18+
enum tReleaseRespStatus {
19+
RELEASE_SUCCESS,
20+
RELEASE_ERROR
21+
}
22+
23+
24+
// event: write lock request (client to lock server)
25+
event eLockReq : tLockReq;
26+
// event: write lock response (lock to client)
27+
event eLockResp : tLockResp;
28+
// event: write release request (client to lock server)
29+
event eReleaseReq : tReleaseReq;
30+
// event: write release response (lock to client)
31+
event eReleaseResp : tReleaseResp;
32+
33+
/*
34+
MutualExclusion specification asserts the following:
35+
1. A lock is acquired only if it is free at that given time
36+
2. A lock is released only when the release request is made by the client that acquires the lock
37+
*/
38+
spec MutualExclusion observes eLockResp, eReleaseResp {
39+
var lockClientPair: map[tLockId, tClientId];
40+
start state WaitForReqAndResp {
41+
on eLockResp do (resp: tLockResp) {
42+
// assert only see lock success if nobody acquired lock at that time
43+
if (resp.lockId in keys(lockClientPair)) {
44+
assert resp.status == LOCK_ERROR, format ("Lock {0} is already acquired, expects lock error but received lock success.", resp.lockId);
45+
}
46+
else {
47+
assert resp.status == LOCK_SUCCESS, format ("Expect success lock lockId: {0} in lock response, but received failed lock.", resp.lockId);
48+
lockClientPair += (resp.lockId, resp.clientId);
49+
}
50+
}
51+
// assert only see release success if the lock is being aquired by the client
52+
on eReleaseResp do (resp: tReleaseResp) {
53+
if (resp.lockId in lockClientPair) {
54+
if (resp.clientId == lockClientPair[resp.lockId]) {
55+
assert resp.status == RELEASE_SUCCESS, format ("Expect success release locId: {0} in release response, but received failed release. rId: {1}", resp.lockId, resp.rId);
56+
lockClientPair -= (resp.lockId);
57+
}
58+
else {
59+
assert resp.status == RELEASE_ERROR, format ("Lock {0} is being acquired by other clients in release request, should have returned release error. rId: {1}", resp.lockId, resp.rId);
60+
}
61+
} else {
62+
assert resp.status == RELEASE_ERROR, format ("Lock {0} in the release request hasn't being acquired yet, should have returned release error. rId: {1}", resp.lockId, resp.rId);
63+
}
64+
}
65+
}
66+
}
67+
68+
/*
69+
ResponseOnlyOnRequest specification asserts the following:
70+
There should be no lock/release response without a corresponding lock/release request
71+
*/
72+
spec ResponseOnlyOnRequest observes eLockReq, eLockResp, eReleaseReq, eReleaseResp {
73+
var pendingLockRequests: map[tLockId, tLockReq];
74+
var pendingReleaseRequests: map[tLockId, tReleaseReq];
75+
76+
start state checking {
77+
on eLockReq do (req: tLockReq) {
78+
pendingLockRequests[req.rId] = req;
79+
}
80+
81+
on eReleaseReq do (req: tReleaseReq) {
82+
pendingReleaseRequests[req.rId] = req;
83+
}
84+
85+
on eReleaseResp do (resp: tReleaseResp) {
86+
assert resp.rId in keys(pendingReleaseRequests), format("rId: {0} was not requested.", resp.rId);
87+
pendingReleaseRequests -= (resp.rId);
88+
}
89+
90+
on eLockResp do (resp: tLockResp) {
91+
assert resp.rId in keys(pendingLockRequests), format("rId: {0} was not requested.", resp.rId);
92+
pendingLockRequests -= (resp.rId);
93+
}
94+
}
95+
}

‎Src/PObserve/Examples/LockServerPObserve/src/main/java/lockserver/pobserve/parser/LockServerParser.java‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
package lockserver.pobserve.parser;
2+
3+
import pobserve.commons.Parser;
4+
import pobserve.commons.PObserveEvent;
5+
import lockserver.pobserve.spec.PEvents;
6+
import lockserver.pobserve.spec.PTypes;
7+
import pobserve.runtime.events.PEvent;
8+
9+
import java.text.ParseException;
10+
import java.text.SimpleDateFormat;
11+
import java.util.HashMap;
12+
import java.util.TimeZone;
13+
import java.util.stream.Stream;
14+
15+
16+
public class LockServerParser implements Parser<PEvent<?>> {
17+
private PEvents.eLockReq onLockReq(long clientID, long lockID, long rId) {
18+
return new PEvents.eLockReq(new PTypes.PTuple_clnt_lock_rId(clientID, lockID, rId));
19+
}
20+
21+
private PEvents.eReleaseReq onReleaseReq(long clientID, long lockID, long rId) {
22+
return new PEvents.eReleaseReq(new PTypes.PTuple_clnt_lock_rId(clientID, lockID, rId));
23+
}
24+
25+
private PEvents.eLockResp onLockRes(long clientID, long lockID, long rId, String result, PTypes.tLockStatus lockStatus) {
26+
PTypes.tLockRespStatus lockRespStatus = null;
27+
if (result.equals("SUCCESS")) {
28+
lockRespStatus = PTypes.tLockRespStatus.LOCK_SUCCESS;
29+
} else if (result.equals("FAIL")) {
30+
lockRespStatus = PTypes.tLockRespStatus.LOCK_ERROR;
31+
}
32+
return new PEvents.eLockResp(new PTypes.PTuple_stts_clnt_lock_lckst_rId(lockRespStatus, clientID, lockID,
33+
lockStatus, rId));
34+
}
35+
36+
private PEvents.eReleaseResp onReleaseRes(long clientID, long lockID, long rId, String result, PTypes.tLockStatus lockStatus) {
37+
PTypes.tReleaseRespStatus releaseRespStatus = null;
38+
if (result.equals("SUCCESS")) {
39+
releaseRespStatus = PTypes.tReleaseRespStatus.RELEASE_SUCCESS;
40+
} else if (result.equals("FAIL")) {
41+
releaseRespStatus = PTypes.tReleaseRespStatus.RELEASE_ERROR;
42+
}
43+
return new PEvents.eReleaseResp(new PTypes.PTuple_stts_clnt_lock_lckst_rId_1(releaseRespStatus, clientID,
44+
lockID, lockStatus, rId));
45+
}
46+
@Override
47+
public Stream<PObserveEvent<PEvent<?>>> apply(Object obj) {
48+
long time;
49+
SimpleDateFormat df = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss.SSSSSS");
50+
String line = (String) obj;
51+
String[] parts = line.split(" - : ");
52+
if (parts.length != 2) {
53+
return Stream.empty();
54+
}
55+
String timestampAndThread = parts[0];
56+
String logInfo = parts[1];
57+
String[] timestampAndThreadParts = timestampAndThread.split(" ");
58+
try {
59+
df.setTimeZone(TimeZone.getTimeZone("UTC"));
60+
time = df.parse(timestampAndThreadParts[0] + " " + timestampAndThreadParts[1]).getTime();
61+
} catch (ParseException e) {
62+
System.out.println("Parsing error: " + e.toString());
63+
return Stream.empty();
64+
}
65+
String[] logInfoParts = logInfo.split(", ");
66+
HashMap<String, String> keyValueMap = new HashMap<>();
67+
for (String part : logInfoParts) {
68+
String[] keyValue = part.split("=");
69+
if (keyValue.length != 2) {
70+
return Stream.empty();
71+
}
72+
keyValueMap.put(keyValue[0], keyValue[1]);
73+
}
74+
return makeEvent(keyValueMap, line, time);
75+
}
76+
77+
public Stream<PObserveEvent<PEvent<?>>> makeEvent(HashMap<String, String> keyValueMap, String line, long time) {
78+
PEvent<?> event = null;
79+
String transactionType = keyValueMap.getOrDefault("TransactionType", "");
80+
String messageType = keyValueMap.getOrDefault("MessageType", "");
81+
long clientID = parseStringValueToLong(keyValueMap.getOrDefault("ClientID", "null"));
82+
long lockID = parseStringValueToLong(keyValueMap.getOrDefault("LockID", "null"));
83+
long rId = parseStringValueToLong(keyValueMap.getOrDefault("TransactionID", "null"));
84+
switch (messageType) {
85+
case "REQUEST":
86+
if (transactionType.equals("LOCK")) {
87+
event = onLockReq(clientID, lockID, rId);
88+
} else if (transactionType.equals("RELEASE")) {
89+
event = onReleaseReq(clientID, lockID, rId);
90+
}
91+
break;
92+
case "RESPONSE":
93+
String result = keyValueMap.getOrDefault("Result", "");
94+
PTypes.tLockStatus lockStatus;
95+
String lockStatusString = keyValueMap.getOrDefault("LockStatus", "null");
96+
if (lockStatusString.equals("null")) {
97+
lockStatus = null;
98+
} else {
99+
lockStatus = PTypes.tLockStatus.valueOf(lockStatusString);
100+
}
101+
if (transactionType.equals("LOCK")) {
102+
event = onLockRes(clientID, lockID, rId, result, lockStatus);
103+
} else if (transactionType.equals("RELEASE")) {
104+
event = onReleaseRes(clientID, lockID, rId, result, lockStatus);
105+
}
106+
default:
107+
break;
108+
}
109+
return event == null ? Stream.empty() : Stream.of(new PObserveEvent<>(Long.toString(lockID), time, event, line));
110+
}
111+
112+
private long parseStringValueToLong(String value) {
113+
return value.equals("null") ? 0 : Long.parseLong(value);
114+
}
115+
}

0 commit comments

Comments
 (0)