au-ts
C-refinement performance
As of a4b5bbcc6, the CorresProof theory for ext2 takes 19 hours to build (on one of the new Precision T1700s).
Running time for all_corres_goals:
66468.986s fsop_dir_mkdir_corres_4
46356.719s deserialise_Ext2Inode_2_corres_4
36024.195s fsop_dir_create_corres_3
9518.724s fs_mount_corres_2
5308.481s ext2_inode_create2_corres_4
5296.032s ext2_inode_create2_corres_3
5294.636s ext2_inode_create2_corres_2
3221.090s get_page_and_iterate_dirents_corres_2
2914.912s ext2_new_block2_corres_2
2874.562s deserialise_Ext2Inode_corres_4
2424.672s get_page_and_check_empty_corres_2
2304.209s fsop_inode_get_block_corres_3
1923.871s ext2_find_entry_bang_corres_3
1802.977s get_page_and_find_space_corres_2
1756.047s get_page_and_find_space_corres_3
[...]
The performance stinks across the board. The current prover re-proves a val_rel at every AST node. The ideal fix would be along the lines of 4dc25e5ce but some thought is needed to deal with the hairy encoding of functions in C-refinement.
The top three all use vfs_inode_set_ops, vfs_inode_set_fileops which each contain a large block of function pointers in a struct, which explains why they're especially bad. val_rel for function pointers involves expanding cdsl_function_val_rel and looking at a few hundred cases.
