Skip to content
This repository has been archived by the owner on Aug 26, 2022. It is now read-only.

update nekara apis #1

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

update nekara apis #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 16 additions & 16 deletions Source/NekaraManagedClient/TestRuntimeApi.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,21 +13,19 @@ public class TestRuntimeApi : ITestingService
[DllImport("nekara.dll")]
public static extern IntPtr CreateScheduler();
[DllImport("nekara.dll")]
public static extern void CreateTask(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void Attach(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void Detach(IntPtr ip);
[DllImport("nekara.dll")]
public static extern bool IsDetached(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void StartTask(IntPtr ip, int _threadID);
public static extern void CreateOperation(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void EndTask(IntPtr ip, int _threadID);
public static extern void StartOperation(IntPtr ip, int _threadID);
[DllImport("nekara.dll")]
public static extern void ContextSwitch(IntPtr ip);
public static extern void EndOperation(IntPtr ip, int _threadID);
[DllImport("nekara.dll")]
public static extern void WaitforMainTask(IntPtr ip);
public static extern void ScheduleNextOperation(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void CreateResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
Expand All @@ -37,11 +35,13 @@ public class TestRuntimeApi : ITestingService
[DllImport("nekara.dll")]
public static extern void BlockedOnAnyResource(IntPtr ip, int[] _resourceID, int _size);
[DllImport("nekara.dll")]
public static extern bool CreateNondetBool(IntPtr ip);
public static extern void BlockedOnResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
public static extern bool GetNextBoolean(IntPtr ip);
[DllImport("nekara.dll")]
public static extern int CreateNondetInteger(IntPtr ip, int _maxvalue);
public static extern int GetNextInteger(IntPtr ip, int _maxvalue);
[DllImport("nekara.dll")]
public static extern void BlockedOnResource(IntPtr ip, int _resourceID);
public static extern void WaitforMainOperation(IntPtr ip);

internal IntPtr ns_handle;

Expand Down Expand Up @@ -72,17 +72,17 @@ public bool IsDetached()

public void CreateTask()
{
CreateTask(ns_handle);
CreateOperation(ns_handle);
}

public void StartTask(int taskId)
{
StartTask(ns_handle, taskId);
StartOperation(ns_handle, taskId);
}

public void EndTask(int taskId)
{
EndTask(ns_handle, taskId);
EndOperation(ns_handle, taskId);
}

public void CreateResource(int resourceId)
Expand Down Expand Up @@ -112,12 +112,12 @@ public void SignalUpdatedResource(int resourceId)

public bool CreateNondetBool()
{
return CreateNondetBool(ns_handle);
return GetNextBoolean(ns_handle);
}

public int CreateNondetInteger(int maxValue)
{
return CreateNondetInteger(ns_handle, maxValue);
return GetNextInteger(ns_handle, maxValue);
}

public void Assert(bool predicate, string s)
Expand All @@ -131,12 +131,12 @@ public void Assert(bool predicate, string s)

public void ContextSwitch()
{
ContextSwitch(ns_handle);
ScheduleNextOperation(ns_handle);
}

public string WaitForMainTask()
{
WaitforMainTask(ns_handle);
WaitforMainOperation(ns_handle);

return "";
}
Expand Down
70 changes: 40 additions & 30 deletions Source/NekaraRpcServer/Core/TestingSession.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,35 +23,31 @@ public class TestingSession : ITestingService
[DllImport("nekara.dll")]
public static extern void NS_WithSeed(int _seed, int max_decisions);
[DllImport("nekara.dll")]
public static extern void NS_CreateTask();
public static extern void CreateOperation(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void NS_StartTask(int _threadID);
public static extern void StartOperation(IntPtr ip, int _threadID);
[DllImport("nekara.dll")]
public static extern void NS_EndTask(int _threadID);
public static extern void EndOperation(IntPtr ip, int _threadID);
[DllImport("nekara.dll")]
public static extern void NS_ContextSwitch();
public static extern void ScheduleNextOperation(IntPtr ip);
[DllImport("nekara.dll")]
public static extern void NS_WaitforMainTask();
public static extern void CreateResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
public static extern void NS_CreateResource(int _resourceID);
public static extern void DeleteResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
public static extern void NS_DeleteResource(int _resourceID);
public static extern void SignalUpdatedResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
public static extern void NS_SignalUpdatedResource(int _resourceID);
public static extern void BlockedOnAnyResource(IntPtr ip, int[] _resourceID, int _size);
[DllImport("nekara.dll")]
public static extern void NS_BlockedOnAnyResource(int[] _resourceID, int _size);
public static extern void BlockedOnResource(IntPtr ip, int _resourceID);
[DllImport("nekara.dll")]
public static extern int NS_GenerateResourceID();
public static extern bool GetNextBoolean(IntPtr ip);
[DllImport("nekara.dll")]
public static extern int NS_GenerateThreadTD();
public static extern int GetNextInteger(IntPtr ip, int _maxvalue);
[DllImport("nekara.dll")]
public static extern bool NS_CreateNondetBool();
public static extern void WaitforMainOperation(IntPtr ip);
[DllImport("nekara.dll")]
public static extern int NS_CreateNondetInteger(int _maxvalue);
[DllImport("nekara.dll")]
public static extern bool NS_Dispose();
[DllImport("nekara.dll")]
public static extern void NS_BlockedOnResource(int _resourceID);
public static extern bool DisposeScheduler();

// It appears that Process.GetCurrentProcess is a very expensive call
// (makes the whole app 10 ~ 15x slower when called in AppendLog), so we save the reference here.
Expand Down Expand Up @@ -502,7 +498,8 @@ public void CreateTask()
programState.InitTaskCreation();
} */

NS_CreateTask();
// TODO: add scheduler ptr
// CreateOperation();
#if DEBUG
stamp = Profiler.Update("CreateTaskEnd", stamp);
#endif
Expand All @@ -528,7 +525,8 @@ public void StartTask(int taskId)
tcs = programState.AddTask(taskId);
} */

NS_StartTask(taskId);
// TODO: add scheduler ptr
// StartOperation(taskId);

#if DEBUG
stamp = Profiler.Update("StartTaskUpdate", stamp);
Expand Down Expand Up @@ -576,7 +574,8 @@ public void EndTask(int taskId)
#endif

// ContextSwitch();
NS_EndTask(taskId);
// TODO: add scheduler ptr
// EndOperation(taskId);

#if DEBUG
stamp = Profiler.Update("EndTaskEnd", stamp);
Expand All @@ -600,7 +599,8 @@ public void CreateResource(int resourceId)
programState.AddResource(resourceId);
} */

NS_CreateResource(resourceId);
// TODO: add scheduler ptr
// CreateResource(resourceId);

#if DEBUG
stamp = Profiler.Update("CreateResourceEnd", stamp);
Expand All @@ -623,7 +623,8 @@ public void DeleteResource(int resourceId)
programState.resourceSet.Remove(resourceId);
} */

NS_DeleteResource(resourceId);
// TODO: add scheduler ptr
// DeleteResource(resourceId);
#if DEBUG
stamp = Profiler.Update("DeleteResourceEnd", stamp);
#endif
Expand Down Expand Up @@ -652,7 +653,8 @@ public void BlockedOnResource(int resourceId)
#if DEBUG
stamp = Profiler.Update("BlockedOnResourceUpdate", stamp);
#endif
NS_BlockedOnResource(resourceId);
// TODO: add scheduler ptr
// BlockedOnResource(resourceId);
// ContextSwitch();
#if DEBUG
stamp = Profiler.Update("BlockedOnResourceEnd", stamp);
Expand Down Expand Up @@ -683,8 +685,8 @@ public void BlockedOnAnyResource(params int[] resourceIds)
#endif

// ContextSwitch();

NS_BlockedOnAnyResource(resourceIds, resourceIds.Length);
// TODO: add scheduler ptr
// BlockedOnAnyResource(resourceIds, resourceIds.Length);
#if DEBUG
stamp = Profiler.Update("BlockedOnResourceEnd", stamp);
#endif
Expand Down Expand Up @@ -712,7 +714,8 @@ public void SignalUpdatedResource(int resourceId)
}
} */

NS_SignalUpdatedResource(resourceId);
// TODO: add scheduler ptr
// SignalUpdatedResource(resourceId);

#if DEBUG
stamp = Profiler.Update("SignalUpdatedResourceEnd", stamp);
Expand All @@ -737,7 +740,9 @@ public bool CreateNondetBool()
return value;
} */

return NS_CreateNondetBool();
// TODO: add scheduler ptr
// return CreateNondetBool();
return false;
}

/// <summary>
Expand All @@ -758,7 +763,9 @@ public int CreateNondetInteger(int maxValue)
return value;
} */

return NS_CreateNondetInteger(maxValue);
// TODO: add scheduler ptr
// return CreateNondetInteger(maxValue);
return 0;
}

/// <summary>
Expand Down Expand Up @@ -909,7 +916,9 @@ public void ContextSwitch()
}
} */

NS_ContextSwitch();

// TODO: add scheduler ptr
// ScheduleNextOperation();
}

/// <summary>
Expand Down Expand Up @@ -947,7 +956,8 @@ public string WaitForMainTask()
try
{
// this.EndTask(0);
NS_WaitforMainTask();
// TODO: add scheduler ptr
// WaitforMainOperation();

programState.RemoveTask(0);
// this.Finish(TestResult.Pass);
Expand Down