create_benchmarks.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import concurrent.futures\n",
    "from multiprocessing.pool import ThreadPool\n",
    "import benchmark\n",
    "import os\n",
    "import syfco\n",
    "import utils\n",
    "import csv\n",
    "import math\n",
    "import json\n",
    "from utils import write_file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "def crawlDir(path):\n",
    "  filtered_files = []\n",
    "  for root, subdirs, files in os.walk(path):\n",
    "    for file in filter(lambda s: s.endswith(\".tlsf\"), files):\n",
    "      full = os.path.join(root, file)\n",
    "      params = syfco.parameters(utils.read_file(full))\n",
    "      if len(params) == 1:\n",
    "        filtered_files.append((full, params[0]))\n",
    "  return filtered_files\n",
    "tlsf_files = crawlDir(\"../../benchmarks/tlsf/\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Not enough realizable examples for amba_case_study\n",
      "Synthesizing amba_decomposed_arbiter\n",
      "Timed out/Errored: amba_decomposed_arbiter\n",
      "Synthesizing amba_decomposed_arbiter\n",
      "Synthesizing amba_decomposed_encode\n",
      "Timed out/Errored: amba_decomposed_encode\n",
      "Synthesizing amba_decomposed_encode\n",
      "Synthesizing amba_decomposed_lock\n",
      "Timed out/Errored: amba_decomposed_lock\n",
      "Synthesizing amba_decomposed_lock\n",
      "Timed out/Errored: amba_decomposed_lock\n",
      "Synthesizing amba_decomposed_lock\n",
      "Timed out/Errored: amba_decomposed_lock\n",
      "Synthesizing amba_decomposed_lock\n",
      "Not enough realizable examples for example10\n",
      "Not enough realizable examples for example10a\n",
      "Not enough realizable examples for example7\n",
      "Not enough realizable examples for example7a\n",
      "Not enough realizable examples for example8\n",
      "Not enough realizable examples for example9\n",
      "Not enough realizable examples for abcg_arbiter\n",
      "Not enough realizable examples for arbiter\n",
      "Not enough realizable examples for arbiter_with_buffer\n",
      "Not enough realizable examples for arbiter_with_cancel\n",
      "Synthesizing collector_v1\n",
      "Timed out/Errored: collector_v1\n",
      "Synthesizing collector_v1\n",
      "Timed out/Errored: collector_v1\n",
      "Not enough realizable examples for collector_v1\n",
      "Synthesizing collector_v2\n",
      "Timed out/Errored: collector_v2\n",
      "Synthesizing collector_v2\n",
      "Synthesizing collector_v3\n",
      "Timed out/Errored: collector_v3\n",
      "Synthesizing collector_v3\n",
      "Synthesizing detector\n",
      "Timed out/Errored: detector\n",
      "Synthesizing detector\n",
      "Timed out/Errored: detector\n",
      "Synthesizing detector\n",
      "Timed out/Errored: detector\n",
      "Synthesizing detector\n",
      "Synthesizing full_arbiter\n",
      "Timed out/Errored: full_arbiter\n",
      "Synthesizing full_arbiter\n",
      "Timed out/Errored: full_arbiter\n",
      "Not enough realizable examples for full_arbiter\n",
      "Not enough realizable examples for full_arbiter_enc\n",
      "Not enough realizable examples for generalized_buffer\n",
      "Not enough realizable examples for lift\n",
      "Not enough realizable examples for lift_unary_enc\n",
      "Not enough realizable examples for lift_wrong_physics_unreal\n",
      "Synthesizing load_balancer\n",
      "Timed out/Errored: load_balancer\n",
      "Synthesizing load_balancer\n",
      "Synthesizing ltl2dba_alpha\n",
      "Timed out/Errored: ltl2dba_alpha\n",
      "Synthesizing ltl2dba_alpha\n",
      "Timed out/Errored: ltl2dba_alpha\n",
      "Synthesizing ltl2dba_alpha\n",
      "Synthesizing ltl2dba_beta\n",
      "Timed out/Errored: ltl2dba_beta\n",
      "Synthesizing ltl2dba_beta\n",
      "Timed out/Errored: ltl2dba_beta\n",
      "Not enough realizable examples for ltl2dba_beta\n",
      "Synthesizing ltl2dba_C2\n",
      "Timed out/Errored: ltl2dba_C2\n",
      "Synthesizing ltl2dba_C2\n",
      "Timed out/Errored: ltl2dba_C2\n",
      "Synthesizing ltl2dba_C2\n",
      "Timed out/Errored: ltl2dba_C2\n",
      "Synthesizing ltl2dba_C2\n",
      "Synthesizing ltl2dba_E\n",
      "Timed out/Errored: ltl2dba_E\n",
      "Synthesizing ltl2dba_E\n",
      "Timed out/Errored: ltl2dba_E\n",
      "Not enough realizable examples for ltl2dba_E\n",
      "Synthesizing ltl2dba_Q\n",
      "Timed out/Errored: ltl2dba_Q\n",
      "Synthesizing ltl2dba_Q\n",
      "Timed out/Errored: ltl2dba_Q\n",
      "Not enough realizable examples for ltl2dba_Q\n",
      "Synthesizing ltl2dba_U1\n",
      "Timed out/Errored: ltl2dba_U1\n",
      "Synthesizing ltl2dba_U1\n",
      "Timed out/Errored: ltl2dba_U1\n",
      "Not enough realizable examples for ltl2dba_U1\n",
      "Synthesizing mux\n",
      "Timed out/Errored: mux\n",
      "Synthesizing mux\n",
      "Timed out/Errored: mux\n",
      "Synthesizing mux\n",
      "Timed out/Errored: mux\n",
      "Synthesizing mux\n",
      "Timed out/Errored: mux\n",
      "Synthesizing mux\n",
      "Synthesizing narylatch\n",
      "Timed out/Errored: narylatch\n",
      "Synthesizing narylatch\n",
      "Synthesizing prioritized_arbiter\n",
      "Timed out/Errored: prioritized_arbiter\n",
      "Synthesizing prioritized_arbiter\n",
      "Synthesizing prioritized_arbiter_enc\n",
      "Timed out/Errored: prioritized_arbiter_enc\n",
      "Synthesizing prioritized_arbiter_enc\n",
      "Timed out/Errored: prioritized_arbiter_enc\n",
      "Not enough realizable examples for prioritized_arbiter_enc\n",
      "Synthesizing round_robin_arbiter\n",
      "Timed out/Errored: round_robin_arbiter\n",
      "Not enough realizable examples for round_robin_arbiter\n",
      "Synthesizing shift\n",
      "Timed out/Errored: shift\n",
      "Synthesizing shift\n",
      "Timed out/Errored: shift\n",
      "Synthesizing shift\n",
      "Timed out/Errored: shift\n",
      "Synthesizing shift\n",
      "Timed out/Errored: shift\n",
      "Synthesizing shift\n",
      "Synthesizing simple_arbiter\n",
      "Timed out/Errored: simple_arbiter\n",
      "Synthesizing simple_arbiter\n",
      "Timed out/Errored: simple_arbiter\n",
      "Synthesizing simple_arbiter\n",
      "Synthesizing simple_arbiter_enc\n",
      "Timed out/Errored: simple_arbiter_enc\n",
      "Synthesizing simple_arbiter_enc\n",
      "[<Benchmark 'amba_decomposed_arbiter'>, <Benchmark 'amba_decomposed_encode'>, <Benchmark 'amba_decomposed_lock'>, <Benchmark 'collector_v2'>, <Benchmark 'collector_v3'>, <Benchmark 'detector'>, <Benchmark 'load_balancer'>, <Benchmark 'ltl2dba_alpha'>, <Benchmark 'ltl2dba_C2'>, <Benchmark 'mux'>, <Benchmark 'narylatch'>, <Benchmark 'prioritized_arbiter'>, <Benchmark 'shift'>, <Benchmark 'simple_arbiter'>, <Benchmark 'simple_arbiter_enc'>]\n"
     ]
    }
   ],
   "source": [
    "import strix\n",
    "import bosy\n",
    "from utils import read_file\n",
    "def get_benchmarks(files) -> list[benchmark.Benchmark]:\n",
    "   bms = []\n",
    "   for (file, param) in files:\n",
    "      (path, name) = os.path.split(file)\n",
    "      (basename, _, _) = name.rpartition(\".\")\n",
    "      csvpath = os.path.join(path, basename + \".csv\")\n",
    "      if not os.path.isfile(csvpath):\n",
    "         continue\n",
    "      with open(csvpath) as csvfile:\n",
    "         spamreader = csv.DictReader(csvfile, dialect=\"unix\")\n",
    "         rows = list(spamreader)\n",
    "         if any(row[\"status\"] == \"unrealizable\" for row in rows): # are any of the benchmarks unrealizable:\n",
    "            continue\n",
    "         realizable_values = sorted(int(row[param]) for row in rows if row[\"status\"] == \"realizable\")\n",
    "\n",
    "         if len(realizable_values) < 2:\n",
    "               print(\"Not enough realizable examples for \" + basename)\n",
    "               continue # not synthesizable for any value of the parameter (or just one)\n",
    "         \n",
    "         maxval = realizable_values[-1]\n",
    "         maxpow2 = pow(2, (maxval).bit_length() - 1)\n",
    "         while (True):\n",
    "            try:\n",
    "               print(\"Synthesizing \" + basename)\n",
    "               bosy.synthesize(\n",
    "                  read_file(file), # spec\n",
    "                  overwrite_params={param: maxpow2 if maxpow2 >= 4 else maxval},\n",
    "                  timeout = 120\n",
    "               )\n",
    "               if maxpow2 < 4:\n",
    "                  examples = realizable_values[-2:] # two largest values\n",
    "                  gen = maxval + 1\n",
    "               else:\n",
    "                  examples = [maxpow2 // 2, maxpow2]\n",
    "                  gen = 2 * maxpow2\n",
    "               bms.append(benchmark.Benchmark({\n",
    "                  \"name\": basename,\n",
    "                  \"params\": [param],\n",
    "                  \"specification\": os.path.abspath(file),\n",
    "                  \"generate\": {param: gen},\n",
    "                  \"implementations\": [{\"params\": {param: n}} for n in examples]\n",
    "               },\"../../benchmarks/tlsf/\"))\n",
    "               break\n",
    "            except:\n",
    "               print(\"Timed out/Errored: \" + basename)\n",
    "               if maxpow2 >= 8:\n",
    "                  maxpow2 = maxpow2 // 2\n",
    "               elif maxpow2 >= 4:\n",
    "                  maxpow2 = maxpow2 // 2\n",
    "                  realizable_values = [v for v in realizable_values if v < maxpow2]\n",
    "                  if len(realizable_values) < 2:\n",
    "                     print(\"Not enough realizable examples for \" + basename)\n",
    "                     break # not synthesizable (under 1m) for any value of the parameter (or just one)\n",
    "                  maxval = realizable_values[-1]\n",
    "               else:\n",
    "                  realizable_values = realizable_values[:-1] #remove biggest parameter\n",
    "                  if len(realizable_values) < 2:\n",
    "                     print(\"Not enough realizable examples for \" + basename)\n",
    "                     break # not synthesizable (under 1m) for any value of the parameter (or just one)\n",
    "                  maxval = realizable_values[-1]\n",
    "               continue            \n",
    "   return bms\n",
    "bms = get_benchmarks(tlsf_files)\n",
    "with open(\"benchmarks_bosy.json\", \"w\") as f:\n",
    "   json.dump(bms, cls=benchmark.BenchmarkEncoder, fp=f, indent=2)\n",
    "print(bms)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "```\n",
    "Not enough realizable examples for amba_case_study\n",
    "Synthesizing amba_decomposed_arbiter\n",
    "Timed out: amba_decomposed_arbiter\n",
    "Synthesizing amba_decomposed_arbiter\n",
    "Synthesizing amba_decomposed_encode\n",
    "Timed out: amba_decomposed_encode\n",
    "Synthesizing amba_decomposed_encode\n",
    "Synthesizing amba_decomposed_lock\n",
    "Timed out: amba_decomposed_lock\n",
    "Synthesizing amba_decomposed_lock\n",
    "Timed out: amba_decomposed_lock\n",
    "Synthesizing amba_decomposed_lock\n",
    "Timed out: amba_decomposed_lock\n",
    "Synthesizing amba_decomposed_lock\n",
    "Not enough realizable examples for example10\n",
    "Not enough realizable examples for example10a\n",
    "Not enough realizable examples for example7\n",
    "Not enough realizable examples for example7a\n",
    "Not enough realizable examples for example8\n",
    "Not enough realizable examples for example9\n",
    "Not enough realizable examples for abcg_arbiter\n",
    "Not enough realizable examples for arbiter\n",
    "Not enough realizable examples for arbiter_with_buffer\n",
    "Not enough realizable examples for arbiter_with_cancel\n",
    "Synthesizing collector_v1\n",
    "Synthesizing collector_v2\n",
    "Synthesizing collector_v3\n",
    "Synthesizing detector\n",
    "Synthesizing full_arbiter\n",
    "Timed out: full_arbiter\n",
    "Synthesizing full_arbiter\n",
    "Not enough realizable examples for full_arbiter_enc\n",
    "Not enough realizable examples for generalized_buffer\n",
    "Not enough realizable examples for lift\n",
    "Not enough realizable examples for lift_unary_enc\n",
    "Not enough realizable examples for lift_wrong_physics_unreal\n",
    "Synthesizing load_balancer\n",
    "Timed out: load_balancer\n",
    "Synthesizing load_balancer\n",
    "Synthesizing ltl2dba_alpha\n",
    "Synthesizing ltl2dba_beta\n",
    "Synthesizing ltl2dba_C2\n",
    "Synthesizing ltl2dba_E\n",
    "Synthesizing ltl2dba_Q\n",
    "Timed out: ltl2dba_Q\n",
    "Synthesizing ltl2dba_Q\n",
    "Synthesizing ltl2dba_U1\n",
    "Synthesizing mux\n",
    "Timed out: mux\n",
    "Synthesizing mux\n",
    "Timed out: mux\n",
    "Synthesizing mux\n",
    "Timed out: mux\n",
    "Synthesizing mux\n",
    "Synthesizing narylatch\n",
    "Synthesizing prioritized_arbiter\n",
    "Synthesizing prioritized_arbiter_enc\n",
    "Timed out: prioritized_arbiter_enc\n",
    "Synthesizing prioritized_arbiter_enc\n",
    "Synthesizing round_robin_arbiter\n",
    "Synthesizing shift\n",
    "Timed out: shift\n",
    "Synthesizing shift\n",
    "Timed out: shift\n",
    "Synthesizing shift\n",
    "Timed out: shift\n",
    "Synthesizing shift\n",
    "Timed out: shift\n",
    "Synthesizing shift\n",
    "Synthesizing simple_arbiter\n",
    "Synthesizing simple_arbiter_enc\n",
    "Timed out: simple_arbiter_enc\n",
    "Synthesizing simple_arbiter_enc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "timeouts = []\n",
    "for bm in bms:\n",
    "  try:\n",
    "    benchmark.build_prompt(bm, mode=\"bosy\")\n",
    "  except e:\n",
    "    print(e)\n",
    "    print(\"timeout: \" + bm.name)\n",
    "    timeouts.append(bm)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": ".venv",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.3"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}