AlgorithmsAreCool

type Timestamp = t: int| 0 <= t <= 9223372036854775808 //2^63

class Entity
{
    var id : string

    predicate isEqual(other : Entity)
        reads this, other
    {
        id == other.id

AlgorithmsAreCool

newtype ThreadId = i: nat | i <= 0xffff_ffff

class Lock
{
    static const NULL_THREAD_ID : ThreadId := 0

    var ownerThread : ThreadId

    constructor()
        ensures ownerThread == NULL_THREAD_ID

AlgorithmsAreCool

using System.Threading.Channels;

using CommunityToolkit.Diagnostics;

using Orleans.Concurrency;

namespace Orleans.Grains.Utility;

public sealed class MessageChannelGrain<T> : Grain, IMessageChannelGrain<T>
{

AlgorithmsAreCool

// See https://aka.ms/new-console-template for more information
using System;
using System.Threading;
using System.Collections.Generic;
using System.Diagnostics.Tracing;
using System.Collections.Concurrent;
using HdrHistogram;
using System.Diagnostics;
using System.Runtime;

AlgorithmsAreCool

Launch parameters:    -l 1
Software:
  Runtime:            .NET Core
    Version:          .NET 8.0.14
    GC mode:          Server GC, Latency mode: Interactive, LOH compaction mode: 0, Large pages: disabled, Generations: 0..2
  OS:                 Microsoft Windows 10.0.19045 (X64)
Hardware:
  CPU:                11th Gen Intel(R) Core(TM) i7-11800H @ 2.30GHz
  CPU core count:     16
  RAM size:           32 GB