From 41b5f9257c6ee37bb31d70360bf2384162a8dee7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Nov 2023 13:21:37 -0800 Subject: [PATCH] Use WebWorkers and add a cache (#1739) --- fiat-html/fiat-crypto.html | 2 +- fiat-html/fiat_crypto_worker.js | 5 ++ fiat-html/main.js | 103 ++++++++++++++++++++++++-------- 3 files changed, 83 insertions(+), 27 deletions(-) create mode 100644 fiat-html/fiat_crypto_worker.js diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html index 819704077c..1d99026ff4 100644 --- a/fiat-html/fiat-crypto.html +++ b/fiat-html/fiat-crypto.html @@ -51,6 +51,7 @@ + @@ -64,7 +65,6 @@ - diff --git a/fiat-html/fiat_crypto_worker.js b/fiat-html/fiat_crypto_worker.js new file mode 100644 index 0000000000..de9f5d8465 --- /dev/null +++ b/fiat-html/fiat_crypto_worker.js @@ -0,0 +1,5 @@ +self.importScripts("fiat_crypto.js"); +self.onmessage = function(e) { + const result = synthesize(e.data); + postMessage(result); +}; diff --git a/fiat-html/main.js b/fiat-html/main.js index 555f06fa9b..8ce7b05346 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -1,4 +1,5 @@ // Written with help from https://chat.openai.com/share/74d5901c-9005-4560-8307-582ff54e403e +const SYNTHESIS_CACHE_VERSION = 1; document.addEventListener('DOMContentLoaded', function() { const errorDiv = document.getElementById('error'); const outputDiv = document.getElementById('output'); @@ -10,6 +11,7 @@ document.addEventListener('DOMContentLoaded', function() { const inputArgs = document.getElementById('inputArgs'); const synthesizeButton = document.getElementById('synthesizeButton'); const cancelButton = document.getElementById('cancelButton'); + const clearCacheButton = document.getElementById('clearCacheButton'); const permalink = document.getElementById('permalink'); const statusSpan = document.getElementById('status'); const isSafari = /^((?!chrome|android).)*safari/i.test(navigator.userAgent); @@ -135,7 +137,7 @@ document.addEventListener('DOMContentLoaded', function() { } } - function handleSynthesisResult(result) { + function handleSynthesisResultData(result) { const success = result[0]; const exceptionText = result[1]; const stdout = result[2]; @@ -168,40 +170,82 @@ document.addEventListener('DOMContentLoaded', function() { updateStatus(""); // Clear status } + function handleSynthesisResult(result, cached) { + const cachedString = cached ? ` (cached on ${result.timestamp})` : ''; + if (result.success) { + clearOutput(); + updateStatus(`Synthesis${cachedString} completed in ${result.time} seconds`); + handleSynthesisResultData(result.result); + } else { + handleException(result.result); + updateStatus(`Synthesis${cachedString} failed in ${result.time} seconds`); + } + } + let synthesisWorker; + + function setupSynthesisWorker() { + synthesisWorker = new Worker("fiat_crypto_worker.js"); + + synthesisWorker.onmessage = function(e) { + console.log(`Early synthesis result: ${e.data}`); + }; + + synthesisWorker.onerror = function(err) { + handleException(err); + }; + } + + function cancelSynthesisWorker() { + if (synthesisWorker) { + synthesisWorker.terminate(); + console.log("Synthesis worker terminated."); + } + setupSynthesisWorker(); // Re-setup the worker for future use + } - var curSynthesisPromise; function handleSynthesis(args) { const startTime = performance.now(); + const cacheKey = 'synthesize_' + JSON.stringify(args); + const cached = localStorage.getItem(cacheKey); console.log({'synthesize args': args}); updateStatus("Synthesizing..."); updatePermalink(args); - const synthesisPromise = new Promise((resolve, reject) => { - try { - resolve(synthesize(args)) - } catch (error) { - reject(error); + + if (cached) { + const cachedData = JSON.parse(cached); + if (cachedData.version === SYNTHESIS_CACHE_VERSION) { + handleSynthesisResult(cachedData, true); + return; + } else { + console.log(`cache miss: version ${cachedData.version}, expected ${SYNTHESIS_CACHE_VERSION}`) } - }); - curSynthesisPromise = synthesisPromise; - synthesisPromise - .then((value) => { - if (curSynthesisPromise === synthesisPromise) { - const endTime = performance.now(); - clearOutput(); - updateStatus(`Synthesis completed in ${(endTime - startTime) / 1000} seconds`); - handleSynthesisResult(value); - } else { - console.log(`Synthesis of ${args} completed after being canceled: ${value}`); - } - }) - .catch((err) => { - if (curSynthesisPromise === synthesisPromise) { - handleException(err); - } else { - console.log(`Synthesis of ${args} errored after being canceled: ${err}`); + } + + const recieveMessage = function (success) { + return function(e) { + const endTime = performance.now(); + const timeTaken = (endTime - startTime) / 1000; + const now = new Date(); + const resultData = { + result: e.data, + time: timeTaken, + success: success, + timestamp: now.toISOString(), + version: SYNTHESIS_CACHE_VERSION + }; + try { + localStorage.setItem(cacheKey, JSON.stringify(resultData)); + } catch (e) { + console.error(`Failed: localStorage.setItem(${JSON.stringify(cacheKey)}, ${JSON.stringify(JSON.stringify(resultData))})`); } - }); + handleSynthesisResult(resultData, false); + }; + }; + + synthesisWorker.postMessage(args); + synthesisWorker.onmessage = recieveMessage(true); + synthesisWorker.onerror = recieveMessage(false); } function parseAndRun(argv) { @@ -214,6 +258,8 @@ document.addEventListener('DOMContentLoaded', function() { } } + setupSynthesisWorker(); + const queryParams = new URLSearchParams(window.location.search); const argv = queryParams.get('argv'); const interactive = queryParams.get('interactive'); @@ -267,5 +313,10 @@ document.addEventListener('DOMContentLoaded', function() { synthesizeButton.disabled = false; cancelButton.disabled = true; updateStatus(""); + cancelSynthesisWorker(); + }); + + clearCacheButton.addEventListener('click', function() { + localStorage.clear(); }); });