Skip to content

Commit

Permalink
update measurements
Browse files Browse the repository at this point in the history
  • Loading branch information
kmill committed May 16, 2024
1 parent c037a22 commit 205143b
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 10 deletions.
4 changes: 2 additions & 2 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -245,8 +245,8 @@ def writeTestImage (filename : String) : IO Unit := do
let width : Nat := 500
let height : Nat := width * 2 / 3
let aspectRatio : Float := (Float.ofNat width) / (Float.ofNat height)
let numThreads := 8
let samplesPerPixel := 10
let numThreads := 10
let samplesPerPixel := 8
let maxDepth := 30

IO.println s!"{numThreads} threads, {width}x{height} pixels, {numThreads*samplesPerPixel} total samples per pixel, max depth {maxDepth}."
Expand Down
9 changes: 3 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,10 @@ Code for writing PPM files originally came from
The raytracer uses `Task`s to render in parallel. Part of a raytracer is using supersampling
to better estimate the amount of light entering each pixel, so it is trivial to parallelize:
the entire image is rendered multiple times, and the results are averaged together.
The following execution times are with respect to an older version of the code, and the new one is
somewhat faster, for example the first test image now takes about 8.5 minutes with the same setup.

![final test image](https://github.com/kmill/lean4-raytracer/blob/master/output/test13.png?raw=true)

(10 minutes with 8 threads on an Intel Xeon E5-2665. 500x333 pixels, 80 total samples per pixel, max depth 30.)
(8 minutes 10 seconds with 10 threads on an Apple M2 Max. 500x333 pixels, 80 total samples per pixel, max depth 30.)

![final test image, higher resolution](https://github.com/kmill/lean4-raytracer/blob/master/output/test13.bigger.png?raw=true)

Expand All @@ -36,6 +34,5 @@ The `c` folder contains an implementation of the raytracer in C, hand translated
This is not meant to be a fair comparison, and I spent more time thinking about optimizing the C version.
The only purpose here is to get some idea of the relative speed of my Lean code.

The first test image in C took 20 seconds with the same configuration, and the second test image took 3 minutes 30 seconds with the same configuration. This means my Lean program takes about 32x as long to run as the C version. (This was using the earlier version of the Lean program. The new one is about 25x.)

The current version incorporates optimizations from the [optimize-lean](https://github.com/kmill/lean4-raytracer/tree/optimize-lean) branch.
The first test image in C took 5.9 seconds with the same configuration,
and the second test image took 1 minute 19 seconds (but with Apple M2 Max).
4 changes: 2 additions & 2 deletions c/render.c
Original file line number Diff line number Diff line change
Expand Up @@ -569,9 +569,9 @@ void write_test_image(const char *filename) {
double aspect_ratio = 3.0 / 2.0;
int width = 500;
int height = (int)(width / aspect_ratio);
int samples_per_pixel = 10;
int samples_per_pixel = 8;
int max_depth = 30;
int num_threads = 8;
int num_threads = 10;

printf("%d threads, %dx%d pixels, %d total samples per pixel, max depth %d.\n",
num_threads, width, height, samples_per_pixel*num_threads, max_depth);
Expand Down

0 comments on commit 205143b

Please sign in to comment.