Vanlightly opened a new issue, #10720: URL: https://github.com/apache/iceberg/issues/10720
### Apache Iceberg version 1.5.2 (latest release) ### Query engine Spark ### Please describe the bug 🐞 I do a lot of formal verification of distributed systems and I have developed a formal specification of Apache Iceberg. The model is based on the read and write logic in the `core` module and the Spark code. The model checker has identified a possible consistency violation when using Serializable isolation, with the combination of copy-on-write mode, with a concurrent delete and compaction. You can find the model and the description of the counterexample here: https://github.com/Vanlightly/table-formats-tlaplus/blob/main/iceberg/README.md#serializable--concurrent-deletecompaction--cow The main issue is that the validation method in BaseRewriteFiles (replace op) only checks for a conflict with new delete files (merge-on-read mode) that reference files logically deleted by the replace operation. However, the counterexample shows that an overwrite operation (copy-on-write mode) that deleted rows could conflict, but no check is performed for that. It's possible I have missed out some check in the formal spec, if so please let me know. I could try to recreate this with tests but I'd like some guidance on how to achieve that as I am new to this codebase. ### Willingness to contribute - [ ] I can contribute a fix for this bug independently - [X] I would be willing to contribute a fix for this bug with guidance from the Iceberg community - [ ] I cannot contribute a fix for this bug at this time -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: issues-unsubscr...@iceberg.apache.org.apache.org For queries about this service, please contact Infrastructure at: us...@infra.apache.org --------------------------------------------------------------------- To unsubscribe, e-mail: issues-unsubscr...@iceberg.apache.org For additional commands, e-mail: issues-h...@iceberg.apache.org
