diff --git a/Source/NekaraManagedClient/TestRuntimeApi.cs b/Source/NekaraManagedClient/TestRuntimeApi.cs index cca9bce..599e693 100644 --- a/Source/NekaraManagedClient/TestRuntimeApi.cs +++ b/Source/NekaraManagedClient/TestRuntimeApi.cs @@ -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")] @@ -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; @@ -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) @@ -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) @@ -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 ""; } diff --git a/Source/NekaraRpcServer/Core/TestingSession.cs b/Source/NekaraRpcServer/Core/TestingSession.cs index 43345e1..eea346b 100644 --- a/Source/NekaraRpcServer/Core/TestingSession.cs +++ b/Source/NekaraRpcServer/Core/TestingSession.cs @@ -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. @@ -502,7 +498,8 @@ public void CreateTask() programState.InitTaskCreation(); } */ - NS_CreateTask(); + // TODO: add scheduler ptr + // CreateOperation(); #if DEBUG stamp = Profiler.Update("CreateTaskEnd", stamp); #endif @@ -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); @@ -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); @@ -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); @@ -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 @@ -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); @@ -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 @@ -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); @@ -737,7 +740,9 @@ public bool CreateNondetBool() return value; } */ - return NS_CreateNondetBool(); + // TODO: add scheduler ptr + // return CreateNondetBool(); + return false; } /// @@ -758,7 +763,9 @@ public int CreateNondetInteger(int maxValue) return value; } */ - return NS_CreateNondetInteger(maxValue); + // TODO: add scheduler ptr + // return CreateNondetInteger(maxValue); + return 0; } /// @@ -909,7 +916,9 @@ public void ContextSwitch() } } */ - NS_ContextSwitch(); + + // TODO: add scheduler ptr + // ScheduleNextOperation(); } /// @@ -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);