diff --git a/external-repository-versions.md b/external-repository-versions.md index d15e02e..c8fe7cf 100644 --- a/external-repository-versions.md +++ b/external-repository-versions.md @@ -55,10 +55,6 @@ Baseline for IronKV. Commit: `2fe4dcdc323b92e93f759cc3e373521366b7f691` -#### Depends on a different version of Verus: https://github.com/verus-lang/verus - -Commit: `96957b633471e4d5a6bc267f9bf0e31555e888db` - ## Other Verifiers ### Creusot: https://github.com/creusot-rs/creusot diff --git a/ironkv/Program.cs b/ironkv/Program.cs new file mode 100644 index 0000000..e218236 --- /dev/null +++ b/ironkv/Program.cs @@ -0,0 +1,233 @@ +using IronfleetCommon; +using IronfleetIoFramework; +using System; +using System.Linq; +using System.Numerics; +using System.Runtime; +using System.Runtime.InteropServices; +using System.Threading; + +namespace IronSHTServer +{ + class Program + { + static void usage() + { + Console.Write(@" +Usage: dotnet IronSHTServer.dll [key=value]... + + - file path of the service description + - file path of the private key + +Allowed keys: + addr - local host name or address to listen to (default: + whatever's specified in the private key file) + port - port to listen to (default: whatever's specified + in the private key file) + profile - print profiling info (false or true, default: false) + verbose - use verbose output (false or true, default: false) +"); + } + + // We make `nc` static so that the C-style callbacks we pass to Verus can use it. + static IoNative.NetClient nc; + + [UnmanagedFunctionPointer(CallingConvention.Cdecl)] + public unsafe delegate void GetMyEndPointDelegate(void** endPoint); + + public unsafe static void GetMyEndPointStatic(void** endPoint) + { + byte[] endPointArray = nc.MyPublicKey(); + byte* endPointBuf; + allocate_buffer((ulong)endPointArray.Length, endPoint, &endPointBuf); + Span endPointSpan = new Span(endPointBuf, endPointArray.Length); + MemoryExtensions.CopyTo(endPointArray, endPointSpan); + } + + [UnmanagedFunctionPointer(CallingConvention.Cdecl)] + public unsafe delegate UInt64 GetTimeDelegate(); + + public unsafe static UInt64 GetTimeStatic() + { + return IoNative.Time.GetTime(); + } + + [UnmanagedFunctionPointer(CallingConvention.Cdecl)] + public unsafe delegate void ReceiveDelegate(int timeLimit, bool *ok, bool *timedOut, void **remote, void **buffer); + + public unsafe static void ReceiveStatic(int timeLimit, bool *ok, bool *timedOut, void **remote, void **buffer) + { + Option rustBuffer; + byte[] remoteArray; + nc.Receive(timeLimit, out *ok, out *timedOut, out remoteArray, out rustBuffer); + if (*ok && !*timedOut) { + if (rustBuffer is Some some) { + byte* remoteBuf; + allocate_buffer((ulong)remoteArray.Length, remote, &remoteBuf); + Span remoteSpan = new Span(remoteBuf, remoteArray.Length); + MemoryExtensions.CopyTo(remoteArray, remoteSpan); + *buffer = some.Value.BoxVecPtr; + } + else { + *remote = null; + *buffer = null; + *ok = false; + } + } + else { + *remote = null; + *buffer = null; + } + } + + [UnmanagedFunctionPointer(CallingConvention.Cdecl)] + public unsafe delegate bool SendDelegate(UInt64 remoteLength, byte *remote, UInt64 bufferLength, byte *buffer); + + public unsafe static bool SendStatic(UInt64 remoteLength, byte *remote, UInt64 bufferLength, byte *buffer) + { + Span remoteSpan = new Span(remote, (int)remoteLength); + Span bufferSpan = new Span(buffer, (int)bufferLength); + return nc.Send(remoteSpan, bufferSpan); + } + + [DllImport("lib.dll")] + public static extern void sht_main_wrapper( + int numArgs, + int[] argLengths, + int totalArgLength, + byte[] flatArgs, + GetMyEndPointDelegate getMyEndPointDelegate, + GetTimeDelegate getTimeDelegate, + ReceiveDelegate receiveDelegate, + SendDelegate sendDelegate + ); + + [DllImport("lib.dll")] + public unsafe static extern void allocate_buffer( + UInt64 length, + void** boxVecPtr, + byte** bufferPtr + ); + + [DllImport("lib.dll")] + public unsafe static extern void free_buffer( + void* boxVecPtr + ); + + static void FlattenArgs(byte[][] args, out byte[] flatArgs, out int[] argLengths) + { + int totalLength = 0; + foreach (var arg in args) { + totalLength += arg.Length; + } + flatArgs = new byte[totalLength]; + argLengths = new int[args.Length]; + int offset = 0; + for (int i = 0; i < args.Length; i++) { + argLengths[i] = args[i].Length; + Array.Copy(args[i], 0, flatArgs, offset, args[i].Length); + offset += args[i].Length; + } + } + + static void Main(string[] args) + { + Console.WriteLine("IronSHTServer program started"); + + Console.WriteLine("Processing command-line arguments"); + + Params ps = new Params(); + + foreach (var arg in args) + { + if (!ps.ProcessCommandLineArgument(arg)) { + usage(); + return; + } + } + + if (!ps.Validate()) { + usage(); + return; + } + + ServiceIdentity serviceIdentity = ServiceIdentity.ReadFromFile(ps.ServiceFileName); + if (serviceIdentity == null) { + return; + } + if (serviceIdentity.ServiceType != "IronSHT") { + Console.Error.WriteLine("ERROR - Service described by {0} is of type {1}, not IronSHT", ps.ServiceFileName, + serviceIdentity.ServiceType); + return; + } + + PrivateIdentity privateIdentity = PrivateIdentity.ReadFromFile(ps.PrivateKeyFileName); + if (privateIdentity == null) { + return; + } + + IoNative.PrintParams.SetParameters(ps.Profile, i_shouldPrintProgress: false); + + RustBufferManager rustBufferManager = new RustBufferManager(); + nc = IoNative.NetClient.Create(privateIdentity, ps.LocalHostNameOrAddress, ps.LocalPort, + serviceIdentity.Servers, rustBufferManager, ps.Verbose, serviceIdentity.UseSsl); + byte[][] serverPublicKeys = serviceIdentity.Servers.Select(server => nc.HashPublicKey(server.PublicKey)).ToArray(); + var ironArgs = serverPublicKeys; + + Profiler.Initialize(); + IoNative.Time.Initialize(); + Console.WriteLine("IronFleet program started."); + Console.WriteLine("[[READY]]"); + byte[] flatArgs; + int[] argLengths; + FlattenArgs(ironArgs, out flatArgs, out argLengths); + unsafe { + sht_main_wrapper(argLengths.Length, argLengths, flatArgs.Length, flatArgs, GetMyEndPointStatic, GetTimeStatic, ReceiveStatic, SendStatic); + } + Console.WriteLine("[[EXIT]]"); + } + } + + public unsafe class RustBuffer + { + private void* boxVecPtr; + private byte* bufferPtr; + private UInt64 length; + + public RustBuffer(void* i_boxVecPtr, byte* i_bufferPtr, UInt64 i_length) + { + boxVecPtr = i_boxVecPtr; + bufferPtr = i_bufferPtr; + length = i_length; + } + + public void* BoxVecPtr { get { return boxVecPtr; } } + public byte* BufferPtr { get { return bufferPtr; } } + public UInt64 Length { get { return length; } } + } + + public class RustBufferManager : BufferManager + { + public unsafe RustBuffer AllocateNewBuffer(UInt64 length) + { + void *boxVecPtr; + byte* bufferPtr; + if (length > Int32.MaxValue) { + throw new Exception("Currently no support for buffers this big"); + } + Program.allocate_buffer(length, &boxVecPtr, &bufferPtr); + return new RustBuffer(boxVecPtr, bufferPtr, length); + } + + public unsafe Span BufferToSpan(RustBuffer buffer) + { + return new Span(buffer.BufferPtr, (int)buffer.Length); + } + + public unsafe void FreeBuffer(RustBuffer buffer) + { + Program.free_buffer(buffer.BoxVecPtr); + } + } +} + diff --git a/ironkv/SConstruct-dafny b/ironkv/SConstruct-dafny new file mode 100644 index 0000000..c2640f8 --- /dev/null +++ b/ironkv/SConstruct-dafny @@ -0,0 +1,373 @@ +# -*- python -*- +import atexit +import os, os.path +import re +import shutil +import subprocess +import sys +import SCons.Util +import threading + +Import("*") + +env = Environment(ENV=os.environ) + +# Retrieve tool-specific command overrides passed in by the user +AddOption('--dafny-path', + dest='dafny_path', + type='string', + default=None, + action='store', + help='Specify the path to Dafny tool binaries') + +AddOption('--no-verify', + dest='no_verify', + default=False, + action='store_true', + help="Don't verify, just build executables") + +AddOption('--time-limit', + dest='time_limit', + type='int', + default=60, + action='store', + help='Specify the time limit to use for each verification') + +dafny_path = GetOption('dafny_path') +if dafny_path is None: + sys.stderr.write("ERROR: Missing --dafny-path on command line\n") + exit(-1) + +if sys.platform == "win32" or sys.platform == "cygwin": + dafny_exe = os.path.join(dafny_path, 'Dafny.exe') + if not os.path.exists(dafny_exe): + print("ERROR: Could not find Dafny executable in " + dafny_path) + exit(-1) + dafny_invocation = [dafny_exe] +else: + dafny_exe = os.path.join(dafny_path, 'Dafny.dll') + if not os.path.exists(dafny_exe): + dafny_exe = os.path.join(dafny_path, 'dafny.dll') + if not os.path.exists(dafny_exe): + print("ERROR: Could not find Dafny executable in " + dafny_path) + exit(-1) + dafny_invocation = ["dotnet", dafny_exe] + +# Useful Dafny command lines +dafny_basic_args = ['/compile:0', '/timeLimit:' + str(GetOption('time_limit')), '/trace'] +dafny_default_args = dafny_basic_args + ['/arith:5', '/noCheating:1'] +dafny_args_nlarith = dafny_basic_args + ['/arith:2', '/noCheating:1'] +dafny_spec_args = dafny_basic_args + +#################################################################### +# +# General routines +# +#################################################################### + +def recursive_glob(env, pattern, strings=False): + matches = [] + split = os.path.split(pattern) # [0] is the directory, [1] is the actual pattern + platform_directory = split[0] #os.path.normpath(split[0]) + for d in os.listdir(platform_directory): + if os.path.isdir(os.path.join(platform_directory, d)): + newpattern = os.path.join(split[0], d, split[1]) + matches.append(recursive_glob(env, newpattern, strings)) + + files = env.Glob(pattern, strings=strings) + matches.append(files) + return Flatten(matches) + +#################################################################### +# +# Make table of special cases requiring non-default arguments +# +#################################################################### + +source_to_args = [ + (r'src/Dafny/Distributed/Protocol/Lock/RefinementProof/RefinementProof\.i\.dfy', dafny_default_args + ['/noNLarith']), + (r'.*nonlinear\.i\.dfy', dafny_args_nlarith), + (r'.*\.s\.dfy', dafny_spec_args), + (r'.*\.dfy', dafny_default_args), +] + +#################################################################### +# +# Dafny-specific utilities +# +#################################################################### + +dafny_include_re = re.compile(r'include\s+"(\S+)"', re.M) +single_line_comments_re = re.compile(r'//.*\n') +multiline_comments_re = re.compile(r'/\*(([^/\*])|(\*[^/])|(/[^\*]))*\*/') + +def remove_dafny_comments(contents): + # Strip out multi-line comments, using a loop to deal with nested comments + while True: + (contents, substitutions_made) = re.subn(multiline_comments_re, ' ', contents) + if substitutions_made == 0: + break + + # Strip out single-line comments + contents = re.sub(single_line_comments_re, '\n', contents) + return contents + +# helper to look up Dafny command-line arguments matching a srcpath, from the +# source_to_args[] dictionary, dealing with POSIX and Windows pathnames, and +# falling back on a default if no specific override is present. +def get_dafny_command_line_args(srcpath): + srcpath = os.path.normpath(srcpath) # normalize the path, which, on Windows, switches to \\ separators + srcpath = srcpath.replace('\\', '/') # switch to posix path separators + for entry in source_to_args: + pattern, args = entry + if re.search(pattern, srcpath, flags=re.IGNORECASE): + return args + + return dafny_default_args + +dependencies_by_file = dict() +already_verified_files = set() +already_printed_files = set() + +# Scan a .dfy file to discover its transitive dependencies, and store a +# list of them in dependencies_by_file[fullpath]. +def recursively_scan_for_dependencies(fullpath, depth): + if fullpath in dependencies_by_file: + return + contents = File(fullpath).get_text_contents() + dirname = os.path.dirname(fullpath) + filename = os.path.basename(fullpath) + contents = remove_dafny_comments(contents) + includes = dafny_include_re.findall(contents) + extra_files = [os.path.abspath(os.path.join(dirname, i)) for i in includes] + transitive_dependencies = set(extra_files) + for srcpath in extra_files: + recursively_scan_for_dependencies(srcpath, depth + 1) + transitive_dependencies.update(dependencies_by_file[srcpath]) + all_dependencies = sorted(list(transitive_dependencies)) + dependencies_by_file[fullpath] = all_dependencies + + +# Scan a .dfy file to discover its dependencies, and add .vdfy targets for each. +def scan_for_more_targets(target, source, env): + node = source[0] + fullpath = str(node) + recursively_scan_for_dependencies(fullpath, 0) + dependencies = dependencies_by_file[fullpath] + for srcpath in dependencies: + if srcpath not in already_verified_files: + f = os.path.splitext(srcpath)[0] + '.vdfy' + env.DafnyVerify(f, [srcpath, dafny_exe]) + already_verified_files.add(srcpath) + return target, source + dependencies + +#################################################################### +# +# Dafny routines +# +#################################################################### + +def check_dafny(lines): + for line in lines: + if re.search("[Oo]ut of resource", line): + sys.stderr.write("Dafny reported an out-of-resource error\n") + raise Exception() + if re.search(r"proof obligations\]\s+errors", line): + sys.stderr.write("Dafny reported errors not in summary\n") + raise Exception() + +def check_and_print_tail(filename): + with open(filename, 'r') as fh: + lines = fh.readlines() + check_dafny(lines) + sys.stdout.write(lines[-1]) + sys.stdout.write('Full check of Dafny output succeeded\n') + +CheckAndPrintTail = SCons.Action.ActionFactory(check_and_print_tail, lambda x: "Checking " + x) + +def generate_dafny_verifier_actions(source, target, env, for_signature): + abs_source = File(source[0]).abspath + abs_target = File(target[0]).abspath + source_name = str(source[0]) + temp_target_file = re.sub(r'\.dfy$', '.tmp', source_name) + args = get_dafny_command_line_args(abs_source) + return [ + dafny_invocation + args + [source_name, ">", temp_target_file], + CheckAndPrintTail(temp_target_file), + Move(abs_target, temp_target_file) + ] + +# Add env.DafnyVerify(), to generate Dafny verifier actions +def add_dafny_verifier_builder(env): + dafny_verifier = Builder(generator = generate_dafny_verifier_actions, + suffix = '.vdfy', + src_suffix = '.dfy', + chdir=0, + emitter = scan_for_more_targets, + ) + env.Append(BUILDERS = {'DafnyVerify' : dafny_verifier}) + +# Verify a set of Dafny files by creating verification targets for each, +# which in turn causes a dependency scan to verify all of their dependencies. +def verify_dafny_files(env, files): + for f in files: + target = os.path.splitext(f)[0] + '.vdfy' + env.DafnyVerify(target, [f, dafny_exe]) + +# Verify *.dfy files in a list of directories. This enumerates +# all files in those trees, and creates verification targets for each, +# which in turn causes a dependency scan to verify all of their dependencies. +def verify_files_in(env, directories): + for d in directories: + files = recursive_glob(env, d+'/*.dfy', strings=True) + verify_dafny_files(env, files) + +def verify_dafny_file(source): + if GetOption('no_verify'): + return + target = re.sub(r"\.dfy$", ".vdfy", source) + env.DafnyVerify(target, [source, dafny_exe]) + +#################################################################### +# +# Dafny compilation +# +#################################################################### + +def generate_dafny_compile_actions(source, target, env, for_signature): + return [ + dafny_invocation + ['/compile:0', '/spillTargetCode:3', '/noVerify', str(source[0])], + ] + +def get_dafny_compile_dependencies(target, source, env): + source_name = str(source[0]) + recursively_scan_for_dependencies(source_name, 0) + verification_dependencies = dependencies_by_file[source_name] + extra_dependencies = verification_dependencies + if not GetOption('no_verify'): + extra_dependencies.extend([re.sub(r'\.dfy$', '.vdfy', f) for f in verification_dependencies if re.search(r'\.dfy$', f)]) + return target, source + extra_dependencies + +# Add env.DafnyCompile(), to generate dafny_compile build actions +def add_dafny_compiler_builder(env): + client_builder = Builder(generator = generate_dafny_compile_actions, + chdir=0, + emitter=get_dafny_compile_dependencies) + env.Append(BUILDERS = {'DafnyCompile' : client_builder}) + +#################################################################### +# +# .NET binaries +# +#################################################################### + +def generate_dotnet_actions(source, target, env, for_signature): + target_dir = os.path.dirname(str(target[0])) + return [ + ["dotnet", "build", "--configuration", "Release", "--output", target_dir, str(source[0])] + ] + +def get_dotnet_dependencies(target, source, env): + csproj_file = str(source[0]) + source_dir = os.path.dirname(csproj_file) + extra_dependencies = [os.path.join(source_dir, f) for f in os.listdir(source_dir) if re.search(r'\.cs$', f)] + with open(csproj_file, 'r') as fh: + for line in fh.readlines(): + m = re.search(r'', line) + if m: + raw_file_name = re.sub(r'\\', '/', m.group(1)) + file_name = os.path.normpath(os.path.join(source_dir, raw_file_name)) + extra_dependencies.append(file_name) + return target, source + extra_dependencies + +# Add env.DotnetBuild(), to generate dotnet build actions +def add_dotnet_builder(env): + client_builder = Builder(generator = generate_dotnet_actions, + chdir=0, + emitter=get_dotnet_dependencies) + env.Append(BUILDERS = {'DotnetBuild' : client_builder}) + + +#################################################################### +# +# Extract verification failure information +# +#################################################################### + +# extract a string filename out of a build failure +def bf_to_filename(bf): + import SCons.Errors + if bf is None: # unknown targets product None in list + return '(unknown tgt)' + elif isinstance(bf, SCons.Errors.StopError): + return str(bf) + elif bf.node: + return str(bf.node) + elif bf.filename: + return bf.filename + return '(unknown failure)' + +def report_verification_failures(): + from SCons.Script import GetBuildFailures + bf = GetBuildFailures() + if bf: + # bf is normally a list of build failures; if an element is None, + # it's because of a target that scons doesn't know anything about. + for x in bf: + if x is not None: + filename = bf_to_filename(x) + if filename.endswith('.vdfy'): + file_to_print = os.path.splitext(filename)[0] + '.tmp' + if os.path.isfile(file_to_print): + sys.stdout.write('\n##### Verification error. Printing contents of ' + file_to_print + ' #####\n\n') + with open (file_to_print, 'r') as myfile: + sys.stdout.write(myfile.read()) + else: + print("ERROR: Verification error, but cannot print output since file %s doesn't exist" % (file_to_print)) + else: + print("Build failure for %s" % (filename)) + + +def display_build_status(): + report_verification_failures() + +#################################################################### +# +# Put it all together +# +#################################################################### + +add_dafny_verifier_builder(env) +add_dafny_compiler_builder(env) +add_dotnet_builder(env) +env.AddMethod(verify_files_in, "VerifyFilesIn") +env.AddMethod(verify_dafny_files, "VerifyDafnyFiles") +atexit.register(display_build_status) + +#################################################################### +# +# Create dependencies +# +#################################################################### + +verify_dafny_file('src/Dafny/Distributed/Services/Lock/Main.i.dfy') +verify_dafny_file('src/Dafny/Distributed/Services/SHT/Main.i.dfy') +verify_dafny_file('src/Dafny/Distributed/Services/RSL/Main.i.dfy') +verify_dafny_file('src/Dafny/Distributed/Protocol/RSL/LivenessProof/LivenessProof.i.dfy') +verify_dafny_file('src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/LivenessProof.i.dfy') + +env.DafnyCompile('src/Dafny/Distributed/Services/RSL/Main.i.cs', 'src/Dafny/Distributed/Services/RSL/Main.i.dfy') +env.DotnetBuild('bin/IronRSLCounterServer.dll', 'src/IronRSLCounterServer/IronRSLCounterServer.csproj') +env.DotnetBuild('bin/IronRSLCounterClient.dll', 'src/IronRSLCounterClient/IronRSLCounterClient.csproj') +env.DotnetBuild('bin/IronRSLKVServer.dll', 'src/IronRSLKVServer/IronRSLKVServer.csproj') +env.DotnetBuild('bin/IronRSLKVClient.dll', 'src/IronRSLKVClient/IronRSLKVClient.csproj') + +env.DafnyCompile('src/Dafny/Distributed/Services/SHT/Main.i.cs', 'src/Dafny/Distributed/Services/SHT/Main.i.dfy') +env.DotnetBuild('bin/IronSHTServer.dll', 'src/IronSHTServer/IronSHTServer.csproj') +env.DotnetBuild('bin/IronSHTClient.dll', 'src/IronSHTClient/IronSHTClient.csproj') + +env.DafnyCompile('src/Dafny/Distributed/Services/Lock/Main.i.cs', 'src/Dafny/Distributed/Services/Lock/Main.i.dfy') +env.DotnetBuild('bin/IronLockServer.dll', 'src/IronLockServer/IronLockServer.csproj') + +env.DotnetBuild('bin/CreateIronServiceCerts.dll', 'src/CreateIronServiceCerts/CreateIronServiceCerts.csproj') +env.DotnetBuild('bin/TestIoFramework.dll', 'src/TestIoFramework/TestIoFramework.csproj') diff --git a/ironkv/SConstruct-verus b/ironkv/SConstruct-verus new file mode 100644 index 0000000..0954cac --- /dev/null +++ b/ironkv/SConstruct-verus @@ -0,0 +1,132 @@ +# -*- python -*- +import atexit +import os, os.path +import re +import shutil +import subprocess +import sys +import SCons.Util +import threading + +Import("*") + +# Retrieve tool-specific command overrides passed in by the user +AddOption('--verus-path', + dest='verus_path', + type='string', + nargs=1, + default=None, + action='store', + help='Specify the path to your local copy of the Verus repo') + +AddOption('--no-verify', + dest='no_verify', + default=False, + action='store_true', + help="Don't verify, just build executables") + +AddOption('--debug-build', + dest='debug_build', + default=False, + action='store_true', + help="Build executables in debug mode") + +verus_path = GetOption('verus_path') +if verus_path is None: + sys.stderr.write("ERROR: Missing --verus-path= on command line\n") + exit(-1) + +#verus_variant = "debug" if GetOption('debug_build') else "release" +verus_variant = "release" +verus_script = os.path.join(verus_path, f"source/target-verus/{verus_variant}/verus") +if sys.platform == 'win32': + verus_script = verus_script + ".exe" +if not os.path.exists(verus_script): + sys.stderr.write("ERROR: Could not find %s\n" % (verus_script)) + exit(-1) + +env = Environment(ENV=os.environ) + +#################################################################### +# +# .NET binaries +# +#################################################################### + +def generate_dotnet_actions(source, target, env, for_signature): + target_dir = os.path.dirname(str(target[0])) + build_config = "Debug" if GetOption('debug_build') else "Release" + return [ + ["dotnet", "build", "--configuration", build_config, "--output", target_dir, str(source[0])] + ] + +def get_dotnet_dependencies(target, source, env): + csproj_file = str(source[0]) + source_dir = os.path.dirname(csproj_file) + extra_dependencies = [os.path.join(source_dir, f) for f in os.listdir(source_dir) if re.search(r'\.cs$', f)] + with open(csproj_file, 'r') as fh: + for line in fh.readlines(): + m = re.search(r'', line) + if m: + raw_file_name = re.sub(r'\\', '/', m.group(1)) + file_name = os.path.normpath(os.path.join(source_dir, raw_file_name)) + extra_dependencies.append(file_name) + return target, source + extra_dependencies + +# Add env.DotnetBuild(), to generate dotnet build actions +def add_dotnet_builder(env): + client_builder = Builder(generator = generate_dotnet_actions, + chdir=0, + emitter=get_dotnet_dependencies) + env.Append(BUILDERS = {'DotnetBuild' : client_builder}) + + +#################################################################### +# +# Verus binaries +# +#################################################################### + +def generate_verus_actions(source, target, env, for_signature): + source_dir = os.path.dirname(str(source[0])) + # [jonh] NB -C opt-level=3 is the default; I don't think it does + # anything here. + # https://users.rust-lang.org/t/do-rust-compilers-have-optimization-flags-like-c-compilers-have/48833/7 + opt_flag = ["-g"] if GetOption('debug_build') else ["-C", "opt-level=3"] + cmd_line = [verus_script, "--crate-type=dylib", "--expand-errors"] + opt_flag + ["--compile", str(source[0])] + if GetOption("no_verify"): + cmd_line.append("--no-verify") + return [ cmd_line ] + +def get_verus_dependencies(target, source, env): + source_dir = os.path.dirname(str(source[0])) + extra_dependencies = [os.path.join(source_dir, f) for f in os.listdir(source_dir) if re.search(r'\.rs$', f)] + return target, source + extra_dependencies + +# Add env.VerusBuild(), to generate Verus build actions +def add_verus_builder(env): + client_builder = Builder(generator = generate_verus_actions, + chdir=0, + emitter=get_verus_dependencies) + env.Append(BUILDERS = {'VerusBuild' : client_builder}) + +#################################################################### +# +# Put it all together +# +#################################################################### + +add_dotnet_builder(env) +add_verus_builder(env) + +#################################################################### +# +# Create dependencies +# +#################################################################### + +env.DotnetBuild('ironsht/bin/IronSHTServer.dll', 'ironsht/csharp/IronSHTServer/IronSHTServer.csproj') +env.DotnetBuild('ironsht/bin/IronSHTClient.dll', 'ironsht/csharp/IronSHTClient/IronSHTClient.csproj') +env.DotnetBuild('ironsht/bin/CreateIronServiceCerts.dll', 'ironsht/csharp/CreateIronServiceCerts/CreateIronServiceCerts.csproj') +env.DotnetBuild('ironsht/bin/TestIoFramework.dll', 'ironsht/csharp/TestIoFramework/TestIoFramework.csproj') +env.VerusBuild('lib.dll', 'ironsht/src/lib.rs') diff --git a/ironkv/compare.py b/ironkv/compare.py index 570d258..fc2dda2 100644 --- a/ironkv/compare.py +++ b/ironkv/compare.py @@ -4,13 +4,13 @@ import sys import time -VERUS_PATH = "C:/Apps/verus-systems-code/ironfleet-comparison/ironsht/bin/" -DAFNY_PATH = "C:/Apps/ironclad-microsoft/ironfleet/bin/" +VERUS_PATH = os.path.join(sys.argv[1], "verified-ironkv/ironsht/bin") +DAFNY_PATH = os.path.join(sys.argv[1], "Ironclad/ironfleet/bin") RAW_DATA_PATH = "raw-data.txt" NUM_THREADS = 10 SECONDS = 30 NUM_KEYS = 1000 -NUM_EXPERIMENT_ITERATIONS = 100 +NUM_EXPERIMENT_ITERATIONS = 10 CONFIDENCE_QUANTILE = 0.95 VALUE_SIZES = [ 128, 256, 512 ] @@ -25,9 +25,11 @@ def launch_server(verus, which_server): "certs/MySHT.IronSHT.service.txt", f"certs/MySHT.IronSHT.server{which_server}.private.txt" ] + print(cmd, file=sys.stderr) server = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) while True: line = server.stdout.readline().decode('utf-8').strip() + # print(f"[server {which_server}]", line, file=sys.stderr) if line == "[[READY]]": return server @@ -47,10 +49,12 @@ def measure_client(verus, workload, value_size): f"numkeys={NUM_KEYS}", f"valuesize={value_size}" ] + print(cmd, file=sys.stderr) client = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) num_requests_completed = 0 while True: line = client.stdout.readline() + # print("[client]", line, file=sys.stderr) if not line: break line = line.decode('utf-8').strip() diff --git a/site/guide.md b/site/guide.md index c630b71..5dd70fe 100644 --- a/site/guide.md +++ b/site/guide.md @@ -464,63 +464,207 @@ results should still (hopefully) confirm our claim of similar performance. ### Instructions -Set 2 requires a Windows x86_64 machine with .NET 5 or newer (we tested .NET 8.0), rust 1.76.0, and python 3. -A reasonably recent laptop or desktop should be sufficient. - -To run this experiment, take the following steps: - -* Build the IronFleet version of IronKV. - * Install `dotnet`. - * Install `scons` with `pip install scons`. - * Download the Dafny 3.4.0 release, including its executable, from - `https://github.com/dafny-lang/dafny/releases/download/v3.4.0/dafny-3.4.0-x64-win.zip`. - * Sync to commit `2fe4dcdc323b92e93f759cc3e373521366b7f691` of the - Ironclad repository at `https://github.com/microsoft/Ironclad.git`. - * From the `ironfleet` directory in that repository, run - `scons --dafny-path=` where `` is the path to the directory - containing the Dafny 3.4.0 executable. -* Build the Verus version of IronKV. - * Download the Verus source code from commit - `96957b633471e4d5a6bc267f9bf0e31555e888db` - of the repo at `https://github.com/verus-lang/verus`. - * Build the Verus source code as the repo describes, making sure to use - `--release` on the `vargo build`. - * Download the Verus version of IronKV from commit - `ea501b56ef92290329ba434fb8b675a5f467de65` of the - repository at `https://github.com/verus-lang/verified-ironkv.git`. - * Make a small local update to that repository's code to make it operate on - Windows, as follows: In the file - `ironsht/csharp/IronSHTClient/Client.cs`, change - all references to `../liblib.so` to `lib.dll`. - * From the top-level directory of that repository, run - `scons --verus-path=` where `` is the path to the root - directory for the Verus repository. This will create a `lib.dll` - file in the top-level directory of that repository. - * Copy that `lib.dll` file to the `ironkv` subdirectory of the repository - for this artifact. For instance, if this file you're reading now is - `/site/guide.md`, copy it to `/ironkv/lib.dll`. -* Prepare to run the experiment. - * Change directory to the `ironkv` subdirectory of the repository for - this artifact. For instance, if this file you're reading now is - `/site/guide.md`, change directory to `/ironkv/`. - * Generate certificates by running - `dotnet /ironsht/bin/CreateIronServiceCerts.dll - outputdir=certs name=MySHT type=IronSHT addr1=127.0.0.1 port1=4001 - addr2=127.0.0.1 port2=4002 addr3=127.0.0.1 port3=4003` - where `` is the path to either the Dafny or Verus IronKV code. - * With `pip`, install `numpy` and `scipy`. - * Update the hardcoded paths `VERUS_PATH` and `DAFNY_PATH` in the script - `compare.py` to match where those directories are on your machine. - * Prepare your machine for the experiment by telling Windows to never - sleep, by telling it to use the "best performance" power mode (to - disable SpeedStep), and by plugging it into a real charging outlet (not - just a USB-C connector to a monitor). -* Run the experiment by running `python compare.py` from the `ironkv` - subdirectory of the repository for this artifact. This will overwrite the - file `raw-data.txt` with its output. +Set 2 requires a Windows x86_64 machine with .NET 6.0, Rust 1.76.0, Python 3, +and Git. A reasonably recent laptop or desktop should be sufficient. For +commands that require a terminal, note that you can open a terminal by +opening the start menu, typing `powershell`, then pressing the enter key. + +#### Setup + +Below you'll find instructions for installing various dependencies. If you +already have a dependency installed, feel free to skip its instructions. But +you may need to reconfigure or reinstall Python 3 or Git to make sure that +it's available in the PATH (i.e., that it can be run from a terminal). + +(Note for artifact evaluators who requested a Windows machine from us: We've +already installed all these dependencies for you.) + +**.NET 6.0**. To install .NET 6.0, go to [https://dotnet.microsoft.com/en-us/download](https://dotnet.microsoft.com/en-us/download) and download **.NET 6.0** for Windows x64. Run the installer. + +**Python 3**. To install Python 3, go to [https://www.python.org/downloads/windows/](https://www.python.org/downloads/windows/), download the latest stable 64-bit installer, and run the installer. +Before selecting "Install now", make sure to choose "Add python.exe to PATH" +at the bottom of the dialog. + +**Rust 1.76.0**. To install Rust 1.76.0, go to https://www.rust-lang.org/tools/install and download "rustup-init.exe (64 bit)". +Run the installer. In the terminal window that appears, if you're asked to +install C++ prerequisites, choose a suitable option. For academic purposes, +you likely want to select Option 1: "Quick Install via the Visual Studio +Community Installer". Install both components: MSVC with C++ build tools, and +the Windows SDK. You can close Visual Studio Community if it opens. In the +terminal window for the Rust setup, select "Customize installation", then +confirm the default triple (`x86_64-pc-windows-msvc`), then choose `1.76.0` when +asked to choose a toolchain. Accept the default profile, accept the request to +modify the PATH, then proceed by pressing enter. When you get the message +"Rust is installed", press the Enter key to exit the setup. + +**Git**. To install Git, go to +[https://git-scm.com/download/win](https://git-scm.com/download/win) and +download "64-bit Git for Windows Setup". Run the installer. You can disable +the "Windows Explorer Integration" feature if you prefer. + +Leave the rest of the configuration as is. In particular, make sure that "Git +from the command line and from 3rd party software" is selected in the dialog +"Adjusting your PATH environment". In the dialog "Configuring the line ending +conversions", make sure "Checkout Windows-style, commit Unix-style line +endings" is selected. You can also choose not to install MinTTY and instead +use the default Windows console. + +#### Additional dependencies and configuration + +Start Powershell by opening the start menu and typing "Powershell" followed by +the Enter key. + +Install `scons` (a build system) by running `pip install scons`. This will only work if python is in the path. + +Make sure git is configured to replace line endings with Windows line endings: `git config --global core.autocrlf true`. + +*Important: Now make a new directory, e.g. "VerusAE", and run the following:* +``` +Set-Variable -Name "VERUS_AE" -Value "C:\Users\Administrator\VerusAE" +``` + +where you replace the path following `-Value` with the path of the newly created "VerusAE" directory. + +#### Clone the repository for this artifact: + +``` +cd $VERUS_AE +git clone -b main --single-branch https://github.com/verus-lang/paper-sosp24-artifact.git verus-sosp24-artifact +cd verus-sosp24-artifact +``` + +#### Build the IronFleet version of IronKV + +* Download the Dafny 3.4.0 release, including its executable, using + ``` + cd $VERUS_AE + $download_url = "https://github.com/dafny-lang/dafny/releases/download/v3.4.0/dafny-3.4.0-x64-win.zip" + Invoke-WebRequest -Uri $download_url -OutFile "$filename.zip" + Expand-Archive -Path "$filename.zip" -DestinationPath "." + Remove-Item "$filename.zip" + ``` + +* Sync to commit `2fe4dcdc323b92e93f759cc3e373521366b7f691` of the + Ironclad repository at `https://github.com/microsoft/Ironclad.git`. + To do this, run the following from a terminal: + ``` + cd $VERUS_AE + git clone https://github.com/microsoft/Ironclad.git + cd Ironclad + git checkout 2fe4dcdc323b92e93f759cc3e373521366b7f691 + ``` + +* Copy the updated SConstruct file from the Artifact Evaluation repo to the ironfleet + directory to make it work with python 3.12, as follows (still in the `Ironclad` directory): + ``` + cp ..\verus-sosp24-artifact\ironkv\SConstruct-dafny .\ironfleet\SConstruct + ``` + +* To build ironclad run the following: + ``` + cd $VERUS_AE/Ironclad/ironfleet + scons --dafny-path=$VERUS_AE\dafny --no-verify + ``` + +#### Build Verus + +* Download the Verus source code from commit + `097ac7ed283ae60375cd9b2b6017b3c629883b2b` + of the repo at `https://github.com/verus-lang/verus`. + To do this, run the following: + ``` + cd $VERUS_AE + git clone https://github.com/verus-lang/verus + cd verus + git checkout 097ac7ed283ae60375cd9b2b6017b3c629883b2b + ``` + +* Build the Verus source code: + ``` + cd source + ..\tools\activate.ps1 + .\tools\get-z3.ps1 + vargo build --release + ``` + +#### Build the Verus version of IronKV + +* Download the Verus version of IronKV from commit + `a593cce3c63c3cb64cbc36039eab217660bc172d` of the + repository at `https://github.com/verus-lang/verified-ironkv.git`. + To do this, run the following: + ``` + cd $VERUS_AE + git clone https://github.com/verus-lang/verified-ironkv.git + cd verified-ironkv + git checkout a593cce3c63c3cb64cbc36039eab217660bc172d + ``` + +* Copy the updated SConstruct file from the Artifact Evaluation repo to the ironfleet + directory to make it work with python 3.12, as follows (still in the `Ironclad` directory): + ``` + cp ..\verus-sosp24-artifact\ironkv\SConstruct-verus SConstruct + ``` + +* We will replace one of the IronKV files to make it operate on + Windows (the main distribution is built for Linux, which exhibits sub-par performance for + the baseline). Proceed as follows: + ``` + cp ..\verus-sosp24-artifact\ironkv\Program.cs ironsht/csharp/IronSHTServer/Program.cs + ``` + You can verify that the only change is for Windows compatibility by running `git diff` here. + +* Build the Verus version of IronKV as follows: + + ``` + scons --verus-path=$VERUS_AE/verus + ``` + This will create a `lib.dll` file in the top-level directory of that repository. + +* Copy that `lib.dll` file to the `ironkv` subdirectory of the repository + for this artifact, as follows: + ``` + cp .\lib.dll ..\verus-sosp24-artifact\ironkv\. + ``` + +#### Prepare to run the experiment. + +* Change directory to the `ironkv` subdirectory of the repository for + this artifact: + ``` + cd $VERUS_AE/verus-sosp24-artifact/ironkv + ``` + +* Generate certificates by running + + ``` + dotnet $VERUS_AE/Ironclad/ironfleet/bin/CreateIronServiceCerts.dll outputdir=certs name=MySHT type=IronSHT addr1=127.0.0.1 port1=4001 addr2=127.0.0.1 port2=4002 addr3=127.0.0.1 port3=4003 + ``` + +* With `pip`, install `numpy` and `scipy`: + + ``` + pip install numpy scipy + ``` + +* If you are on a laptop, prepare your machine for the experiment by + telling Windows to never sleep, by telling it to use the "best performance" power mode + (to disable SpeedStep), and by plugging it into a real charging outlet (not + just a USB-C connector to a monitor). + +* Run the experiment by running + ``` + cd $VERUS_AE/verus-sosp24-artifact/ironkv + python compare.py $VERUS_AE + ``` + This will overwrite the file `raw-data.txt` with its output. + * Generate the graph by running `python gengraph.py > ironfleet-port-plot.tex`. This uses the data stored in `raw-data.txt` to generate a graph, in LaTeX - format, in the file `ironfleet-port-plot.tex`. + format, in the file `ironfleet-port-plot.tex`. You can include this in a + LaTeX document that uses packages `tikz` and `pgfplots` and build it. Or, if + you just want to manually inspect its contents, you can read the lines + enclosed by \addplot commands to see the values that would be plotted. ## Set 3 - Node Replication