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

Commit

Permalink
CreateMachineIdFromString API and tests (#368)
Browse files Browse the repository at this point in the history 
* CreateMachineIdFromString API and tests

* More tests

* Some bookkeeping

* minor updates

* changed CreateMachineIdFromString to CreateMachineIdFromName

* fixes in tests from my changes
  • Loading branch information
@akashlal
akashlal committed Sep 25, 2018
1 parent ca824f2 commit c6a4441
Show file tree
Hide file tree
Showing 7 changed files with 617 additions and 70 deletions.
103 changes: 40 additions & 63 deletions Source/Core/Runtime/Machines/MachineId.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,24 +15,22 @@ namespace Microsoft.PSharp
[DataContract]
public sealed class MachineId
{
#region fields

/// <summary>
/// The P# runtime that executes the machine with this id.
/// </summary>
public PSharpRuntime Runtime { get; private set; }

/// <summary>
/// Name of the machine.
/// Unique id, when <see cref="NameValue"/> is empty.
/// </summary>
[DataMember]
public readonly string Name;
public readonly ulong Value;

/// <summary>
/// Optional friendly name of the machine.
/// Unique id, when non-empty.
/// </summary>
[DataMember]
private readonly string FriendlyName;
public readonly string NameValue;

/// <summary>
/// Type of the machine with this id.
Expand All @@ -41,10 +39,10 @@ public sealed class MachineId
public readonly string Type;

/// <summary>
/// Unique id value.
/// Name of the machine used for logging.
/// </summary>
[DataMember]
public readonly ulong Value;
public readonly string Name;

/// <summary>
/// Generation of the runtime that created this machine id.
Expand All @@ -58,66 +56,49 @@ public sealed class MachineId
[DataMember]
public readonly string Endpoint;

#endregion

#region constructors
/// <summary>
/// True if <see cref="NameValue"/> is used as the unique id, else false.
/// </summary>
public bool IsNameUsedForHashing => NameValue.Length > 0;

/// <summary>
/// Creates a new machine id.
/// </summary>
/// <param name="type">Machine type</param>
/// <param name="friendlyName">Friendly machine name</param>
/// <param name="runtime">PSharpRuntime</param>
internal MachineId(Type type, string friendlyName, PSharpRuntime runtime)
/// <param name="useNameForHashing">Use friendly name as the id</param>
internal MachineId(Type type, string friendlyName, PSharpRuntime runtime, bool useNameForHashing = false)
{
FriendlyName = friendlyName;
Runtime = runtime;
Endpoint = Runtime.NetworkProvider.GetLocalEndpoint();

// Atomically increments and safely wraps into an unsigned long.
Value = (ulong)Interlocked.Increment(ref runtime.MachineIdCounter) - 1;

// Checks for overflow.
Runtime.Assert(Value != ulong.MaxValue, "Detected MachineId overflow.");

Generation = runtime.Configuration.RuntimeGeneration;

Type = type.FullName;
if (friendlyName != null && friendlyName.Length > 0)
if (useNameForHashing)
{
Name = string.Format("{0}({1})", friendlyName, Value);
Value = 0;
NameValue = friendlyName;
Runtime.Assert(!string.IsNullOrEmpty(NameValue), "Input friendlyName cannot be null when used as Id");
}
else
{
Name = string.Format("{0}({1})", Type, Value);
}
}
// Atomically increments and safely wraps into an unsigned long.
Value = (ulong)Interlocked.Increment(ref runtime.MachineIdCounter) - 1;
NameValue = string.Empty;

/// <summary>
/// Create a fresh MachineId borrowing information from a given id.
/// </summary>
/// <param name="mid">MachineId</param>
internal MachineId(MachineId mid)
{
Runtime = mid.Runtime;
Endpoint = mid.Endpoint;

// Atomically increments and safely wraps into an unsigned long.
Value = (ulong)Interlocked.Increment(ref Runtime.MachineIdCounter) - 1;

// Checks for overflow.
Runtime.Assert(Value != ulong.MaxValue, "Detected MachineId overflow.");
// Checks for overflow.
Runtime.Assert(Value != ulong.MaxValue, "Detected MachineId overflow.");
}

Generation = mid.Generation;
Type = mid.Type;
Generation = runtime.Configuration.RuntimeGeneration;

if (FriendlyName != null && FriendlyName.Length > 0)
Type = type.FullName;
if (IsNameUsedForHashing)
{
Name = string.Format("{0}({1})", FriendlyName, Value);
Name = NameValue;
}
else
else
{
Name = string.Format("{0}({1})", Type, Value);
Name = string.Format("{0}({1})", string.IsNullOrEmpty(friendlyName) ? Type : friendlyName, Value);
}
}

Expand All @@ -129,10 +110,6 @@ internal void Bind(PSharpRuntime runtime)
{
Runtime = runtime;
}

#endregion

#region generic public and override methods

/// <summary>
/// Determines whether the specified System.Object is equal
Expand All @@ -142,18 +119,20 @@ internal void Bind(PSharpRuntime runtime)
/// <returns>Boolean</returns>
public override bool Equals(object obj)
{
if (obj == null)
if (obj is MachineId mid)
{
return false;
// Use same machanism for hashing.
if (IsNameUsedForHashing != mid.IsNameUsedForHashing)
{
return false;
}

return IsNameUsedForHashing ?
NameValue.Equals(mid.NameValue) && Generation == mid.Generation :
Value == mid.Value && Generation == mid.Generation;
}

MachineId mid = obj as MachineId;
if (mid == null)
{
return false;
}

return Value == mid.Value && Generation == mid.Generation;
return false;
}

/// <summary>
Expand All @@ -163,7 +142,7 @@ public override bool Equals(object obj)
public override int GetHashCode()
{
int hash = 17;
hash = hash * 23 + Value.GetHashCode();
hash = hash * 23 + (IsNameUsedForHashing ? NameValue.GetHashCode() : Value.GetHashCode());
hash = hash * 23 + Generation.GetHashCode();
return hash;
}
Expand All @@ -176,7 +155,5 @@ public override string ToString()
{
return Name;
}

#endregion
}
}
11 changes: 11 additions & 0 deletions Source/Core/Runtime/PSharpRuntime.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,17 @@ private void Initialize()

public MachineId CreateMachineId(Type type, string friendlyName = null) => new MachineId(type, friendlyName, this);

/// <summary>
/// Creates a machine id that is uniquely tied to the specified unique name. The
/// returned machine id can either be a fresh id (not yet bound to any machine),
/// or it can be bound to a previously created machine. In the second case, this
/// machine id can be directly used to communicate with the corresponding machine.
/// </summary>
/// <param name="type">Type of the machine</param>
/// <param name="uniqueName">Unique name used to create the machine id</param>
/// <returns>MachineId</returns>
public abstract MachineId CreateMachineIdFromName(Type type, string uniqueName);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and with
/// the specified optional <see cref="Event"/>. This event can only be
Expand Down
11 changes: 11 additions & 0 deletions Source/Core/Runtime/ProductionRuntime.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,17 @@ private void Initialize()

#region runtime interface

/// <summary>
/// Creates a machine id that is uniquely tied to the specified unique name. The
/// returned machine id can either be a fresh id (not yet bound to any machine),
/// or it can be bound to a previously created machine. In the second case, this
/// machine id can be directly used to communicate with the corresponding machine.
/// </summary>
/// <param name="type">Type of the machine</param>
/// <param name="uniqueName">Unique name used to create the machine id</param>
/// <returns>MachineId</returns>
public override MachineId CreateMachineIdFromName(Type type, string uniqueName) => new MachineId(type, uniqueName, this, true);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and with
/// the specified optional <see cref="Event"/>. This event can only be
Expand Down
25 changes: 24 additions & 1 deletion Source/TestingServices/Runtime/TestingRuntime.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,11 @@ internal sealed class TestingRuntime : PSharpRuntime
/// </summary>
private ConcurrentDictionary<int, Machine> TaskMap;

/// <summary>
/// Map that stores all unique names and their corresponding machine ids.
/// </summary>
internal ConcurrentDictionary<string, MachineId> NameValueToMachineId;

/// <summary>
/// Set of all machine Ids created by this runtime.
/// </summary>
Expand Down Expand Up @@ -147,12 +152,30 @@ private void Initialize()
this.TaskMap = new ConcurrentDictionary<int, Machine>();
this.RootTaskId = Task.CurrentId;
this.AllCreatedMachineIds = new HashSet<MachineId>();
this.NameValueToMachineId = new ConcurrentDictionary<string, MachineId>();
}

#endregion

#region runtime interface

/// <summary>
/// Creates a machine id that is uniquely tied to the specified unique name. The
/// returned machine id can either be a fresh id (not yet bound to any machine),
/// or it can be bound to a previously created machine. In the second case, this
/// machine id can be directly used to communicate with the corresponding machine.
/// </summary>
/// <param name="type">Type of the machine</param>
/// <param name="uniqueName">Unique name used to create the machine id</param>
/// <returns>MachineId</returns>
public override MachineId CreateMachineIdFromName(Type type, string uniqueName)
{
// It is important that all machine ids use the monotonically incrementing
// value as the id during testing, and not the unique name.
var mid = new MachineId(type, uniqueName, this);
return this.NameValueToMachineId.GetOrAdd(uniqueName, mid);
}

/// <summary>
/// Creates a new machine of the specified type and with
/// the specified optional event. This event can only be
Expand Down Expand Up @@ -218,7 +241,7 @@ internal MachineId CreateMachine(MachineId mid, Type type, string friendlyName,

return this.CreateMachine(mid, type, friendlyName, e, creator, operationGroupId);
}

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and name, and
/// with the specified optional <see cref="Event"/>. This event can only be
Expand Down

0 comments on commit c6a4441

Please sign in to comment.