wolfspider/GCTypes.c

wolfspider · 2024-08-04T07:17:51Z

Rust embeds a lot of safety checks within the binary which is presumably what you would want if the program is modified outside of the author's control possibly. Formal verification can do those checks as well and it doesn't have to be embedded within the application itself. They both represent two different approaches and some of the newest advancements incorporate both by formally verifying Rust within the context of a provable methodology. All of these insights were gathered via the following Low* code:

module GcTypes

open FStar.HyperStack.ST

module U32 = FStar.UInt32

let test (): Stack (list U32.t) (fun _ -> true) (fun _ _ _ -> true) =
  0ul :: 1ul :: []

let main (): Stack FStar.Int32.t (fun _ -> true) (fun _ _ _ -> true) =
  match test () with
  | x :: y :: [] ->
      FStar.Int.Cast.uint32_to_int32 FStar.UInt32.(x +%^ y -%^ 1ul)
  | _ ->
      FStar.Int.Cast.uint32_to_int32 1ul

wolfspider · 2024-10-02T17:53:32Z

After switching to a more modern machine let's put this all together for the final results. We should know what to expect here:

───────┬────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
       │ File: gcTypesCpp.cpp
───────┼────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
   1   │ #include <optional>
   2   │ #include <list>
   3   │ #include <array>
   4   │ #include <iostream>
   5   │
   6   │ using namespace std;
   7   │
   8   │ int main()
   9   │ {
  10   │
  11   │     for(int I; I < 50000000; ++I)
  12   │     {
  13   │
  14   │         list<optional<array<int, 1>>> sourceList {
  15   │         array<int, 1>{0},
  16   │         array<int, 1>{1},
  17   │         {},
  18   │         array<int, 1>{1},
  19   │         array<int, 1>{0}
  20   │         };
  21   │
  22   │
  23   │         list<optional<array<int, 1>>> copiedList(sourceList);
  24   │     };
  25   │
  26   │     return 0;
  27   │ }
  28   │
───────┴────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────

❯ time ./gcTypesCpp
./gcTypesCpp  25.21s user 0.02s system 99% cpu 25.230 total
❯ time ./gcTypesCpp01
./gcTypesCpp01  0.00s user 0.00s system 85% cpu 0.004 total

C++ using std does this operation in 25 seconds but O1 optimizes it out completely and only increments the counter.

(edit: I've decided to follow up and measure this on the same machine by forcing C++ not to optimize. At that point it is doing something different but interesting to look at the performance at any rate.)

───────┬──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
       │ File: gcTypesCpp-NonOpt.cpp
───────┼──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
   1   │ #include <optional>
   2   │ #include <list>
   3   │ #include <array>
   4   │ #include <iostream>
   5   │ 
   6   │ using namespace std;
   7   │ 
   8   │ volatile int sink = 0; // Prevent optimization by introducing a volatile sink
   9   │ 
  10   │ int main() {
  11   │     for (int I = 0; I < 50000000; ++I) {
  12   │         list<optional<array<int, 1>>> sourceList{
  13   │             array<int, 1>{0},
  14   │             array<int, 1>{1},
  15   │             {},
  16   │             array<int, 1>{1},
  17   │             array<int, 1>{0}
  18   │         };
  19   │ 
  20   │         list<optional<array<int, 1>>> copiedList(sourceList);
  21   │ 
  22   │         // Introduce a side effect using a volatile variable
  23   │         sink += copiedList.size();
  24   │     };
  25   │ 
  26   │     return 0;
  27   │ }
───────┴──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────

❯ clang++ -std=c++17 gcTypesCpp-NonOpt.cpp -O3 -o gcTypesCpp-NonOpt
❯ time ./gcTypesCpp-NonOpt
./gcTypesCpp-NonOpt  5.91s user 0.00s system 99% cpu 5.912 total

───────┬────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
       │ File: src/main.rs
───────┼────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
   1   │ #![feature(box_patterns)]
   2   │
   3   │ #[allow(dead_code)]
   4   │ #[derive(Clone)] // Deriving Clone for the enum
   5   │ enum List {
   6   │     Nil,
   7   │     Cons(u32, Box<List>),
   8   │ }
   9   │
  10   │ fn test() -> List {
  11   │     List::Cons(0, Box::new(List::Cons(1, Box::new(List::Nil))))
  12   │ }
  13   │
  14   │ fn main() {
  15   │     for _i in 1..50000000 {
  16   │         let _list = test();
  17   │
  18   │         let _copieidlist = test().clone();
  19   │     }
  20   │ }
───────┴────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────

❯ time cargo run src/main.rs
   Compiling rust-list-test v0.1.0 (/home/jessebennett/rust-list-test)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.07s
     Running `target/debug/rust-list-test src/main.rs`
cargo run src/main.rs  10.12s user 0.07s system 100% cpu 10.152 total

───────┬────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
       │ File: src/main.rs
───────┼────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
   1   │ #![feature(box_patterns)]
   2   │
   3   │ //#[allow(dead_code)]
   4   │ #[derive(Clone)] // Deriving Clone for the enum
   5   │ enum List {
   6   │     Nil,
   7   │     Cons(u32, Box<List>),
   8   │ }
   9   │
  10   │ fn test() -> List {
  11   │     List::Cons(0, Box::new(List::Cons(1, Box::new(List::Nil))))
  12   │ }
  13   │
  14   │ fn main() {
  15   │     for _i in 1..50000000 {
  16   │         let _list = test();
  17   │
  18   │         let _copieidlist = test().clone();
  19   │     }
  20   │ }
───────┴────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────

❯ time cargo run --release src/main.rs
   Compiling rust-list-test v0.1.0 (/home/jessebennett/rust-list-test)
warning: fields `0` and `1` are never read
 --> src/main.rs:7:10
  |
7 |     Cons(u32, Box<List>),
  |     ---- ^^^  ^^^^^^^^^
  |     |
  |     fields in this variant
  |
  = note: `List` has a derived impl for the trait `Clone`, but this is intentionally ignored during dead code analysis
  = note: `#[warn(dead_code)]` on by default
help: consider changing the fields to be of unit type to suppress this warning while preserving the field numbering, or remove the fields
  |
7 |     Cons((), ()),
  |          ~~  ~~

warning: `rust-list-test` (bin "rust-list-test") generated 1 warning
    Finished `release` profile [optimized] target(s) in 0.08s
     Running `target/release/rust-list-test src/main.rs`
cargo run --release src/main.rs  3.12s user 0.05s system 100% cpu 3.151 total

Testing Rust opts shows that the execution time is cut down by ~70% but yet still clocks in at 3 seconds and still does not optimize the loop out entirely. It is initially faster than the unoptimized C++ by ~250%.

───────┬────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
       │ File: gcTypes.c
───────┼────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
   1   │ #include <stdlib.h>
   2   │ #include <stdint.h>
   3   │ #include <stdio.h>
   4   │
   5   │ // Define the list structure
   6   │ typedef struct Prims_list__uint32_t {
   7   │     enum { Prims_Cons, Prims_Nil, Prims_Null } tag;
   8   │     union {
   9   │         struct {
  10   │             struct Prims_list__uint32_t *tl;
  11   │             uint32_t hd[1];
  12   │         };
  13   │         struct {
  14   │             struct Prims_list__uint32_t *ntl;
  15   │             uint32_t nd[];
  16   │         };
  17   │     };
  18   │ } Prims_list__uint32_t;
  19   │
  20   │ // Function to create a new Cons node
  21   │ Prims_list__uint32_t *cons(uint32_t hd, Prims_list__uint32_t *tl) {
  22   │     Prims_list__uint32_t *node = (Prims_list__uint32_t *)malloc(sizeof(Prims_list__uint32_t));
  23   │     node->tag = Prims_Cons;
  24   │     node->hd[1] = hd;
  25   │     node->tl = tl;
  26   │     return node;
  27   │ }
  28   │
  29   │ Prims_list__uint32_t *ncons(Prims_list__uint32_t *tl) {
  30   │     Prims_list__uint32_t *node = (Prims_list__uint32_t *)malloc(sizeof(Prims_list__uint32_t));
  31   │     node->tag = Prims_Null;
  32   │     node->ntl = tl;
  33   │     return node;
  34   │ }
  35   │
  36   │ // Function to create a new Nil node
  37   │ Prims_list__uint32_t *nil() {
  38   │     Prims_list__uint32_t *node = (Prims_list__uint32_t *)malloc(sizeof(Prims_list__uint32_t));
  39   │     node->tag = Prims_Nil;
  40   │     node->tl = NULL;
  41   │     return node;
  42   │ }
  43   │
  44   │ // Deep copy function
  45   │ Prims_list__uint32_t *deep_copy_list(Prims_list__uint32_t *list) {
  46   │     if (list == NULL) {
  47   │         return NULL;
  48   │     }
  49   │
  50   │     if (list->tag == Prims_Nil) {
  51   │         return nil();
  52   │     }
  53   │
  54   │     if (list->tag == Prims_Null) {
  55   │
  56   │         Prims_list__uint32_t *new_list = ncons(NULL);
  57   │
  58   │         new_list->tl = deep_copy_list(list->ntl);
  59   │
  60   │         return new_list;
  61   │     }
  62   │
  63   │     // Create a new node and copy the head value
  64   │     Prims_list__uint32_t *new_list = cons(list->hd[1], NULL);
  65   │
  66   │     // Recursively copy the rest of the list
  67   │     new_list->tl = deep_copy_list(list->tl);
  68   │
  69   │     return new_list;
  70   │ }
  71   │
  72   │ // Free list function for cleanup
  73   │ void free_list(Prims_list__uint32_t *list) {
  74   │
  75   │     if(list->tag == Prims_Null) {
  76   │         while (list != NULL) {
  77   │             Prims_list__uint32_t *next = list->ntl;
  78   │             free(list);
  79   │             list = next;
  80   │        }
  81   │     }
  82   │     else {
  83   │         while (list != NULL) {
  84   │             Prims_list__uint32_t *next = list->tl;
  85   │             free(list);
  86   │             list = next;
  87   │         }
  88   │     }
  89   │ }
  90   │
  91   │ // Print list function
  92   │ void print_list(Prims_list__uint32_t *list) {
  93   │     printf("[");
  94   │     while (list != NULL) {
  95   │         if (list->tag == Prims_Cons) {
  96   │             printf("%u", list->hd[1]);
  97   │             list = list->tl;
  98   │             if (list != NULL) {
  99   │                 printf(" -> ");
 100   │             }
 101   │         } else if (list->tag == Prims_Nil) {
 102   │             printf("Nil");
 103   │             list = list->tl;
 104   │             if (list != NULL) {
 105   │                 printf(" -> ");
 106   │             }
 107   │         } else if (list->tag == Prims_Null) {
 108   │             printf("Null");
 109   │             list = list->ntl;
 110   │             if (list != NULL) {
 111   │                 printf(" -> ");
 112   │             }
 113   │         }
 114   │     }
 115   │     printf("]\n");
 116   │ }
 117   │
 118   │ // Test the deep copy function
 119   │ int main() {
 120   │
 121   │     for(int I = 0; I < 50000000; ++I)
 122   │     {
 123   │         // Create an example list: 0 -> 1 -> Null -> 1 -> 0 -> Nil
 124   │         Prims_list__uint32_t *original_list = cons(0, cons(1, ncons(cons(1, cons(0, nil())))));
 125   │
 126   │         Prims_list__uint32_t *copied_list = deep_copy_list(original_list);
 127   │
 128   │         free_list(original_list);
 129   │
 130   │         free_list(copied_list);
 131   │     }
 132   │
 133   │     return 0;
 134   │ }
───────┴────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────

❯ time ./gcTypes
./gcTypes  6.68s user 0.00s system 99% cpu 6.686 total
❯ time ./gcTypes01
./gcTypes01  5.19s user 0.00s system 99% cpu 5.191 total

And finally we have C with light assistance from Low*. At 6.68s this is the fastest bar-none. I have even left in the code for the full implementation just as these other languages are pulling in the entire libraries to accomplish the same thing. Optimization shaves 1 second off and then it becomes the slowest but no effort has been made to actually do anything about that. This is just one test and many languages are multi-faceted when it comes to performance but these consistent results are showing the value of formal verification. I will leave you with wise words from one of the luminaries of my time who went by the name "Biggie Smalls":

You can be as good as the best of them. But as bad as the worst, so don't test me (Get money) You better move over (Get money)

Notorious B.I.G, Young M.A.F.I.A., Gettin' Money (Get Money Remix)

wolfspider/GCTypes.c

Select an option

No results found

Select an option

No results found

wolfspider commented Aug 4, 2024

Uh oh!

wolfspider commented Oct 2, 2024 •

edited

Loading

Uh oh!

	#include <stdlib.h>
	#include <stdint.h>
	#include <stdio.h>

	// Define the list structure
	typedef struct Prims_list__uint32_t {
	enum { Prims_Cons, Prims_Nil, Prims_Null } tag;
	union {
	struct {
	struct Prims_list__uint32_t *tl;
	uint32_t hd[1];
	};
	struct {
	struct Prims_list__uint32_t *ntl;
	uint32_t nd[];
	};
	};
	} Prims_list__uint32_t;

	// Function to create a new Cons node
	Prims_list__uint32_t cons(uint32_t hd, Prims_list__uint32_t tl) {
	Prims_list__uint32_t node = (Prims_list__uint32_t )malloc(sizeof(Prims_list__uint32_t));
	node->tag = Prims_Cons;
	node->hd[1] = hd;
	node->tl = tl;
	return node;
	}

	Prims_list__uint32_t ncons(Prims_list__uint32_t tl) {
	Prims_list__uint32_t node = (Prims_list__uint32_t )malloc(sizeof(Prims_list__uint32_t));
	node->tag = Prims_Null;
	node->ntl = tl;
	return node;
	}

	// Function to create a new Nil node
	Prims_list__uint32_t *nil() {
	Prims_list__uint32_t node = (Prims_list__uint32_t )malloc(sizeof(Prims_list__uint32_t));
	node->tag = Prims_Nil;
	node->tl = NULL;
	return node;
	}

	// Deep copy function
	Prims_list__uint32_t deep_copy_list(Prims_list__uint32_t list) {
	if (list == NULL) {
	return NULL;
	}

	if (list->tag == Prims_Nil) {
	return nil();
	}

	if (list->tag == Prims_Null) {

	Prims_list__uint32_t *new_list = ncons(NULL);

	new_list->tl = deep_copy_list(list->ntl);

	return new_list;
	}

	// Create a new node and copy the head value
	Prims_list__uint32_t *new_list = cons(list->hd[1], NULL);

	// Recursively copy the rest of the list
	new_list->tl = deep_copy_list(list->tl);

	return new_list;
	}

	// Free list function for cleanup
	void free_list(Prims_list__uint32_t *list) {

	if(list->tag == Prims_Null) {
	while (list != NULL) {
	Prims_list__uint32_t *next = list->ntl;
	free(list);
	list = next;
	}
	}
	else {
	while (list != NULL) {
	Prims_list__uint32_t *next = list->tl;
	free(list);
	list = next;
	}
	}
	}

	// Print list function
	void print_list(Prims_list__uint32_t *list) {
	printf("[");
	while (list != NULL) {
	if (list->tag == Prims_Cons) {
	printf("%u", list->hd[1]);
	list = list->tl;
	if (list != NULL) {
	printf(" -> ");
	}
	} else if (list->tag == Prims_Nil) {
	printf("Nil");
	list = list->tl;
	if (list != NULL) {
	printf(" -> ");
	}
	} else if (list->tag == Prims_Null) {
	printf("Null");
	list = list->ntl;
	if (list != NULL) {
	printf(" -> ");
	}
	}
	}
	printf("]\n");
	}

	// Test the deep copy function
	int main() {
	// Create an example list: 0 -> 1 -> Null -> 1 -> 0 -> Nil
	Prims_list__uint32_t *original_list = cons(0, cons(1, ncons(cons(1, cons(0, nil())))));

	// Print the original list
	printf("Original list: ");
	print_list(original_list);

	// Deep copy the list
	Prims_list__uint32_t *copied_list = deep_copy_list(original_list);

	// Print the copied list
	printf("Copied list: ");
	print_list(copied_list);

	// Free the original list
	free_list(original_list);

	// Free the copied list
	free_list(copied_list);

	return 0;
	}

wolfspider/GCTypes.c

wolfspider commented Aug 4, 2024

Uh oh!

wolfspider commented Oct 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

wolfspider commented Oct 2, 2024 •

edited

Loading