{"action":"created","issue":{"url":"https://api.github.com/repos/klee/klee/issues/904","repository_url":"https://api.github.com/repos/klee/klee","labels_url":"https://api.github.com/repos/klee/klee/issues/904/labels{/name}","comments_url":"https://api.github.com/repos/klee/klee/issues/904/comments","events_url":"https://api.github.com/repos/klee/klee/issues/904/events","html_url":"https://github.com/klee/klee/pull/904","id":326807366,"number":904,"title":"Change run.stats file format to sqlite3","user":{"login":"kren1","id":310855,"avatar_url":"https://avatars3.githubusercontent.com/u/310855?v=4","gravatar_id":"","url":"https://api.github.com/users/kren1","html_url":"https://github.com/kren1","followers_url":"https://api.github.com/users/kren1/followers","following_url":"https://api.github.com/users/kren1/following{/other_user}","gists_url":"https://api.github.com/users/kren1/gists{/gist_id}","starred_url":"https://api.github.com/users/kren1/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kren1/subscriptions","organizations_url":"https://api.github.com/users/kren1/orgs","repos_url":"https://api.github.com/users/kren1/repos","events_url":"https://api.github.com/users/kren1/events{/privacy}","received_events_url":"https://api.github.com/users/kren1/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-05-27T11:12:12Z","updated_at":"2018-05-27T13:12:09Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/klee/klee/pulls/904","html_url":"https://github.com/klee/klee/pull/904","diff_url":"https://github.com/klee/klee/pull/904.diff","patch_url":"https://github.com/klee/klee/pull/904.patch"},"body":"This pull request changes the file format used to store run.stats file to sqlite3.\r\n\r\nDisadvantage:\r\n 1. *run.stats no longer human readable*: I would consider the current format to be human-non-readable, but with this you can't open it in a text editor.\r\n\r\nAdvantages:\r\n 1. *smaller run.stats file size*: Sqlite3 is a binary format which immediately reduces filesize. Furthermore it uses variable length encoding for integers, so it can use less than `numberOfRecords * numberOfFields * widthOfFields` bytes\r\n1. *faster writes*: In most uses cases it should write faster than the current method (see below)\r\n1. *faster klee-stats*: `klee-stats` gets very slow in my experience when dealing with `run.stats` with a lot of records, moving to sqlite3 should enable this to be much faster. I didn't benchmark  `klee-stats` in this PR, because that is a seprate issue\r\n1. *SQL query lagnuage*: performing ad-hoc queries is much easier. You can just run `sqlite3 klee-last/run.stats` and type whatever SQL query you have in mind\r\n1. *Well defined fail behaviour*:  I don't think it's currently well defined what stats are written if KLEE crashes. SQLIte enables us to control this (the trade-off is performance)\r\n\r\n\r\n## Performance\r\n\r\nI performed a small scale benchmark, similar to what KLEE does,, where I write 13 `int` records into a table. I can get 1M writes/s, but only about 1K/s commits on my machine. That means we can have very fast writes (that is writes on every instruction), but we can't commit on every instruction. \r\n\r\nSo I can up with the following scheme:\r\n* If we write on interval we commit for every write \r\n* If we write on instructions, we commit for every 1000 writes\r\n* User can override the above settings with whatever they want\r\n\r\nThis gives sensible (fast) defaults, but still enables slow reliable per instruction writes.\r\n\r\nI also ran a `od.bc` dumping a concrete file with ` -stats-write-after-instructions=1 -stats-write-interval=0`, both with and without this patch. For some reason me and @MartinNowack  couldn't get KLEE to execute the same number of instructions on this benchmark, but SQLite3 seems to do more work in the same time:\r\n\r\nCVS:\r\n```\r\nKLEE: done: total instructions = 4656860\r\nKLEE: done: completed paths = 1\r\nKLEE: done: generated tests = 1\r\n\r\nreal    0m24.402s\r\nuser    0m18.408s\r\nsys     0m5.980s\r\nn$ ls -lh klee-last/run.stats\r\n-rw-r--r-- 1 tk1713 srg 648M May 27 11:51 klee-last/run.stats\r\n```\r\n\r\nSQLite:\r\n```\r\nKLEE: done: total instructions = 5361184\r\nKLEE: done: completed paths = 1\r\nKLEE: done: generated tests = 1\r\n\r\nreal    0m24.787s\r\nuser    0m20.428s\r\nsys     0m4.344s\r\n$ ls -lh klee-last/run.stats\r\n-rw-r--r-- 1 tk1713 srg 247M May 27 11:53 klee-last/run.stats\r\n```\r\n\r\n## Grafana \r\n\r\nThis was inspired by @251 talk on Grafana. Unfortunately Grafana doesn't support SQLite as datasource (yet, maybe?), but I think this gets us closer to there. We just need to implement a [simple json datasource](https://github.com/grafana/simple-json-datasource), which is a webserver that queries the database a bit. I think this is much easier to do on top of SQLite than a CSV file. There is even a [blog post](https://nbsoftsolutions.com/blog/replacing-elasticsearch-with-rust-and-sqlite) about it.\r\n\r\n## klee-stats\r\n\r\nI've only changed klee-stats in a minimal way to support what I think is the common use case. I don't want this to be bogged down because of `klee-stats`, so I think there are 3 options:\r\n\r\n* Delete all the complicated code from `klee-stats` and support only the core.\r\n* Conform to the current LazyList implementation, but this involved reading in the whole database and would give poor performance.\r\n* Decide what nice to have features we want in `klee-stats` (without referring to the current implementation). I'm not sure what people use, but I would keep only the `--print-*` options and add some nice interface to SQL like `klee-stats -s 'SELECT * FROM stats WHERE ... ORDER BY ...'`\r\n"},"comment":{"url":"https://api.github.com/repos/klee/klee/issues/comments/392330115","html_url":"https://github.com/klee/klee/pull/904#issuecomment-392330115","issue_url":"https://api.github.com/repos/klee/klee/issues/904","id":392330115,"user":{"login":"kren1","id":310855,"avatar_url":"https://avatars3.githubusercontent.com/u/310855?v=4","gravatar_id":"","url":"https://api.github.com/users/kren1","html_url":"https://github.com/kren1","followers_url":"https://api.github.com/users/kren1/followers","following_url":"https://api.github.com/users/kren1/following{/other_user}","gists_url":"https://api.github.com/users/kren1/gists{/gist_id}","starred_url":"https://api.github.com/users/kren1/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kren1/subscriptions","organizations_url":"https://api.github.com/users/kren1/orgs","repos_url":"https://api.github.com/users/kren1/repos","events_url":"https://api.github.com/users/kren1/events{/privacy}","received_events_url":"https://api.github.com/users/kren1/received_events","type":"User","site_admin":false},"created_at":"2018-05-27T13:12:09Z","updated_at":"2018-05-27T13:12:09Z","author_association":"CONTRIBUTOR","body":"@251 Sure, but I don't think it fits in this PR. Also the problematic options are `--sort-by`, `--ascending`, `'--compare-by`,  `'--compare-at`, `--draw-line-chart'`.\r\n\r\n@ccadar  We had a discusison about this on Friday after the meeting  @251 and @MartinNowack so I wanted to support my argument with some benchmarks, then I though I might as well do a PR out of it.\r\n\r\nI don't think YAML solves the problem of storing and querying data, so I'm not sure what you mean, but here are some thought:\r\n\r\n* Encoding rows in YAML format: That would make it a lot more verbose and perhaps more readable, but would make much larger files. Also it's schema-less, but we have a schema that doesn't change while KLEE is running. I don't see a reason we would want rows with different fields in the same run.stats file.\r\n\r\n*  Maybe we could store YAML encoded rows in a NoSQL database, but KLEE doesn't generate nearly enough data to warant one. They are harder to setup and maintain (I don't want to install and setup one just to run KLEE). Querying is also more annoying usually.\r\n\r\n\r\nSQLite is very close to the current implementation, it just gives formal structure to the data (which we alreadz have but don't enforce), it has a well known language to query it (so we don't have to reinvent the wheel with klee-stats) and is a sensible database (instead of the wild west with files)"}}
{"actor":{"display_login":"kren1"}}