Model Checking of Linearizability of Concurrent List Implementations